damiano
damiano
The logic of the linter is as follows. First, a linter is a command that takes the syntax of each command and does something with it. (Really, a linter can...
> Also: should the linter move to `Mathlib/Tactic/Linter`? (Did the [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2FTactic.2F*) come to a conclusion?) That discussion did not come to a conclusion...
bors r+
No, currently it is "declaration" based.
Actually, I do not think that `#find_home` can be run on a file either: `#find_home` takes an identifier as input (which is legal also for `#min_imps`). Moreover, `#min_imps` takes any...
bors merge
@kmill, I am happy that you mention this! I had also thought of using the `InfoTrees`, but I still feel a little intimidated by them, so I resorted to the...
Ok, I will experiment with `InfoTrees`. I would like to understand them better anyway, since they would be useful for the "beginners linter" flagging `Nat.sub`: I want that linter to...
I had not been exhaustive about golfing, since I wanted to not clutter too much the PR with the definition. I'm very happy that, now that the definitions are in,...
Relavant [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/vscode-lean4.20RFC.3A.20Auto-surround.20text.20with.20.60.24.60.20in.20markdown/with/523491953).