linting

Stream: condensed mathematics

[Johan Commelin]

wc -l scripts/nolints.txt
227 scripts/nolints.txt

I've been cleaning up linting problems yesterday. There's lots of declarations with unused arguments, wrong priorities, instances flagged by the fails_quickly linter, etc...
If you have some time on your hands, feel free to help. It might help with speeding up some of the files.

[Riccardo Brasca]

In practice you go through any single line there and see if you can fix it by hand?

[Johan Commelin]

The linter is complaining about unused arguments. If anyone wants to help make the linter happy, here is the repot:
https://github.com/leanprover-community/lean-liquid/runs/7318103732?check_suite_focus=true#step:5:21

[Johan Commelin]

I'll not touch the project for an hour now.

[Riccardo Brasca]

I can do it.

[Riccardo Brasca]

Some of them are done.