lean4-htt/tests/plugin
larsk21 cf4e106304 fix: unused variables linter review comments
- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
2022-06-03 13:03:52 +02:00
..
.gitignore feat: stop compiling Lean code as C++, remove --cpp option 2020-05-14 14:45:33 +02:00
SnakeLinter.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
SnakeLinter.lean.expected.out chore: fix test 2021-01-27 15:04:59 +01:00
test_single.sh fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00