lean4-htt/src/Lean/Parser
2021-09-07 17:50:34 -07:00
..
Attr.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Basic.lean refactor: lazy evaluation for >>, <*>, <*, and *> 2021-09-07 17:50:34 -07:00
Command.lean feat: elaborate optional deriving after def 2021-09-03 10:22:17 -07:00
Do.lean fix: count quotation depth in parser correctly 2021-04-29 13:33:48 +02:00
Extension.lean fix: update tokenTable at withNamespace parser combinator 2021-08-23 09:41:36 -07:00
Extra.lean chore: use register_parser_alias where possible 2021-07-22 16:28:06 +02:00
Level.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Module.lean chore: rebase and rm rawPos 2021-08-03 09:13:18 +02:00
StrInterpolation.lean chore: fix parser error message 2021-04-24 21:48:12 +02:00
Syntax.lean feat: allow user to set "behavior" at declare_syntax_cat 2021-09-01 13:28:12 -07:00
Tactic.lean feat: add (generalizing := true/false) optional attribute to match 2021-04-15 17:04:25 -07:00
Term.lean chore: add binop_lazy% 2021-09-07 13:00:36 -07:00