search

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

chore: test file for linting lean4 #871

Closed semorrison closed 1 month ago

semorrison commented 2 months ago

Adds a file in test/ for running the environment linters on lean4 itself.

Everything is commented out, because it is too slow to run in Batteries CI, and there are still many failures. Nevertheless it is useful to have a coordinated place to run these linters from, until such a time as we can move environment linters up.

I have addressed many in

I have not touched the explicitVarsOfIff linter, but I would be happy to review a PR making progress on this.