leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

doc: fix outdated docstring #880

Closed grunweg closed 1 month ago

grunweg commented 1 month ago

The unusedHavesSuffices linter is run by default now: remove the part of its docstring which says otherwise.

grunweg commented 1 month ago

awaiting-review