lean4-htt/src/Init/Lean/Parser
2020-01-16 17:51:01 -08:00
..
Command.lean refactor: uniform precedence representation 2020-01-15 20:53:23 -08:00
Identifier.lean
Level.lean fix: Level parser 2020-01-14 18:43:42 -08:00
Module.lean chore: move Message to Lean 2020-01-10 10:58:50 -08:00
Parser.lean feat: add support for trailing syntax 2020-01-15 20:53:23 -08:00
Syntax.lean chore: minor 2020-01-15 20:53:24 -08:00
Tactic.lean feat: allow underscore to be used as identifier 2020-01-16 17:51:01 -08:00
Term.lean fix: infixR helper only works for termParsers 2020-01-14 18:06:57 -08:00
Transform.lean