Sebastian Ullrich c9713b1b69 fix: setExpectedFn		2022-03-02 16:28:53 +01:00
..
Attr.lean	chore: remove parser! and tparser!	2021-03-11 09:36:58 -08:00
Basic.lean	fix: setExpectedFn	2022-03-02 16:28:53 +01:00
Command.lean	feat: process termination_by syntax	2022-01-12 16:15:30 -08:00
Do.lean	feat: modify notation for providing motive in "match" expressions	2022-02-14 15:36:14 -08:00
Extension.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00
Extra.lean	feat: add ppRealFill and ppRealGroup combinators	2021-12-15 11:42:38 +00:00
Level.lean	chore: remove parser! and tparser!	2021-03-11 09:36:58 -08:00
Module.lean	feat: add info field to Syntax.node	2021-10-26 20:19:27 +02:00
StrInterpolation.lean	chore: fix parser error message	2021-04-24 21:48:12 +02:00
Syntax.lean	feat: indentation sensitiviy for macro and elab commands	2021-10-18 17:16:09 -07:00
Tactic.lean	feat: modify notation for providing motive in "match" expressions	2022-02-14 15:36:14 -08:00
Term.lean	feat: add pp annotation for match parser	2022-02-14 15:46:52 -08:00