lean4-htt/src/Lean/Parser
2020-06-11 16:18:26 -07:00
..
Command.lean chore: remove unnecessary [appPrec] annotations 2020-06-10 14:44:54 -07:00
Level.lean chore: appPrec => maxPrec 2020-06-10 16:50:09 -07:00
Module.lean
Parser.lean doc: update comments to match new algorithm 2020-06-11 16:18:26 -07:00
Syntax.lean feat: add notationItem 2020-06-10 16:54:46 -07:00
Tactic.lean chore: make sure parser! and tparser! use a syntax similar to the one used at syntax for setting precedences 2020-06-10 16:09:13 -07:00
Term.lean chore: remove checkWsBeforeIfSymbol hack 2020-06-11 14:58:29 -07:00
Transform.lean