Extend getChecks to allow an additional list of linters, which is always run. This can be used downstream to e.g. enable the docBlameThm or explicitVarsOfIff linters without modifying batteries.
As part of this, we
update fix the function docstring (which was quite outdated anyway)
remove the useOnly option: the equivalent effect can be achieved by filtering the list of linters afterwards; adding linters cannot, hence must be performed in this function. (That said, I'm happy to add this functionality back if desired.)
rename a variable dflt to the more readable default
adjust the logic of the #lint command accordingly
Note that test/lint_simpNF.lean lies on this (the docBlame linter warns there) - so this changed is already tested.
Extend
getChecks
to allow an additional list of linters, which is always run. This can be used downstream to e.g. enable thedocBlameThm
orexplicitVarsOfIff
linters without modifying batteries.As part of this, we
useOnly
option: the equivalent effect can be achieved by filtering the list of linters afterwards; adding linters cannot, hence must be performed in this function. (That said, I'm happy to add this functionality back if desired.)dflt
to the more readabledefault
test/lint_simpNF.lean
lies on this (the docBlame linter warns there) - so this changed is already tested.