New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: ignore def
/theorem
confusion in docBlame
#269
fix: ignore def
/theorem
confusion in docBlame
#269
Conversation
Some `def`s are generated by core and should really be theorems; we treat them as such in the `docBlame` and `docBlameThm` linters.
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
test? |
There was already a test for |
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Is there an issue for this on the lean4 repository? I can't find one. It would be good to link to such an issue from the code here, even it is linking to a |
I'm not aware of one. I'd prefer to get this merged soon, as the sooner this is merged the sooner we stop receiving useless comments like
in mathlib |
I think you should open a tracking issue and link to it from this PR. |
Co-authored-by: Scott Morrison <scott@tqft.net>
Created by running `lake exe runLinter --update Mathlib` locally. Most changes are due to leanprover/std4#269: proof fields in classes or structures do not require a docstring any more.
Some
def
s are generated by core and should really be theorems; we treat them as such in thedocBlame
anddocBlameThm
linters.This fixes #217.