lean4-htt/src/Lean/Parser
Leonardo de Moura abf78e162c feat: add notation for disabling implicit lambda feature
This notation will be useful for writing macros where
implicit lambdas are not desired.
2021-04-12 22:33:23 -07:00
..
Attr.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Basic.lean fix: error recovery at sepBy combinator 2021-04-05 18:38:57 -07:00
Command.lean feat: parser alias for 'declVal' 2021-04-12 16:59:54 -07:00
Do.lean feat: introduce arg precedence 2021-03-22 16:33:37 +01:00
Extension.lean chore: implement lhs prec 2021-03-22 16:33:37 +01:00
Extra.lean fix: do not use nullKind for group combinator 2021-04-07 22:30:51 -07:00
Level.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Module.lean fix: ignore syntactically incorrect commands that do not contain any symbol 2021-04-07 14:46:13 -07:00
StrInterpolation.lean feat: nicer token parse errors 2021-03-14 08:23:32 -07:00
Syntax.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Tactic.lean chore: remove parser! and tparser! 2021-03-11 09:36:58 -08:00
Term.lean feat: add notation for disabling implicit lambda feature 2021-04-12 22:33:23 -07:00