Leonardo de Moura d56163bd0e refactor: resolveNamespace now return a List		2022-06-16 17:16:36 -07:00
..
Attr.lean	chore: remove parser! and tparser!	2021-03-11 09:36:58 -08:00
Basic.lean	fix: adapt to stricter grammar	2022-06-16 23:33:57 +02:00
Command.lean	refactor: move linebreak check into sepBy(1)Indent	2022-06-16 23:33:57 +02:00
Do.lean	feat: let/if indentation in do blocks	2022-06-13 16:18:49 -07:00
Extension.lean	refactor: resolveNamespace now return a List	2022-06-16 17:16:36 -07:00
Extra.lean	refactor: move linebreak check into sepBy(1)Indent	2022-06-16 23:33:57 +02:00
Level.lean	chore: remove parser! and tparser!	2021-03-11 09:36:58 -08:00
Module.lean	fix: skip antiquotations during parser recovery	2022-04-27 10:41:27 +02:00
StrInterpolation.lean	refactor: make String.Pos opaque	2022-03-20 10:47:13 -07:00
Syntax.lean	feat: indentation sensitiviy for macro and elab commands	2021-10-18 17:16:09 -07:00
Tactic.lean	chore: enforce naming convetion for tactics	2022-03-30 16:19:05 -07:00
Term.lean	refactor: move linebreak check into sepBy(1)Indent	2022-06-16 23:33:57 +02:00