mathlib3
036c96bf - fix(tactic/lint): _ is not a linter (#8634)

Commit
4 years ago
fix(tactic/lint): _ is not a linter (#8634) The `#lint` parser accepts `ident_`, but as far as I can tell, `_` doesn't mean anything in particular, it just tries and fails to resolve the `linter._` linter. This simplifies the parser to only accept `ident`.
Author
Parents
Loading