lean4-htt/doc/examples
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
..
compiler
NFM2022 doc: add slide headers to examples 2022-05-23 18:20:37 -07:00
bintree.lean doc: fix typo gree -> tree 2022-05-09 09:44:48 +02:00
bintree.lean.md
deBruijn.lean chore: missing backtick 2022-04-10 11:11:51 -07:00
deBruijn.lean.md
interp.lean
interp.lean.md
palindromes.lean chore: typos 2022-04-09 13:02:01 -07:00
palindromes.lean.md
phoas.lean chore: remove unnecessary annotation 2022-04-06 16:38:16 -07:00
phoas.lean.md
tc.lean chore: break long lines 2022-04-06 16:37:38 -07:00
tc.lean.md
test_single.sh fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00