damiano
damiano
In particular, I would rather this be opt-in: I would like this to be in place for latex files, but I would prefer if this were not the default behaviour...
That's true: it was not easy to get the test file to work, since I could not save it! Would the "script-style" code below be better than a linter, then?...
Michael, thank you for the suggestion: I like it and I renamed the script to `declarations_diff`.
I love this, thanks! I just have one comment: would it be possible to have links external to `leanprover-community` to open in a separate tab? Maybe this already happens, but...
You don't even need the list: ```lean4 def ohno (x : Fin 2) : Nat := match x with | ⟨0, _⟩ => sorry | 1 => sorry | x...
Thank! :octopus: bors merge