lean4-htt/src/Lean/Parser
Leonardo de Moura b0564a32b9 feat: add AttrM
We are going to use `AttrM` to implement solution 2 described at https://github.com/leanprover/lean4/issues/175
2020-09-21 16:44:20 -07:00
..
Basic.lean chore: add quotedCharCoreFn 2020-09-20 17:05:47 -07:00
Command.lean feat: add initialize command parser 2020-09-20 13:42:50 -07:00
Extension.lean feat: add AttrM 2020-09-21 16:44:20 -07:00
Level.lean chore: universe-+ spacing 2020-09-17 08:12:28 -07:00
Module.lean fix: skip minimum amount of tokens during parser recovery 2020-09-21 11:37:50 +02:00
Syntax.lean feat: add support for parser priorities in the syntax command 2020-09-19 18:47:08 -07:00
Tactic.lean chore: cleanup 2020-09-19 09:24:50 -07:00
Term.lean feat: formatter: use hard space after opening structure instance brace 2020-09-18 13:15:40 -07:00
Transform.lean chore: Lean.Parser.Parser ~> Lean.Parser.Basic 2020-08-13 18:44:13 +02:00