max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Linter
History
Leonardo de Moura 30d625697e chore: use Expr.forEachWhere to implement linter 
closes #1899

TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities.
2022-11-30 18:44:20 -08:00
..
Basic.lean feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00
Builtin.lean feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00
Deprecated.lean feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00
MissingDocs.lean feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00
UnusedVariables.lean chore: use Expr.forEachWhere to implement linter 2022-11-30 18:44:20 -08:00
Util.lean feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00