Leonardo de Moura e52a7bdf42 feat: let/if indentation in do blocks ... closes #1120		2022-06-13 16:18:49 -07:00
..
Attr.lean	chore: remove parser! and tparser!	2021-03-11 09:36:58 -08:00
Basic.lean	feat: let/if indentation in do blocks	2022-06-13 16:18:49 -07:00
Command.lean	chore: update whereStructInst	2022-06-07 18:41:43 -07:00
Do.lean	feat: let/if indentation in do blocks	2022-06-13 16:18:49 -07:00
Extension.lean	chore: unused variables	2022-06-07 17:54:10 -07:00
Extra.lean	fix: inconsistency between syntax and kind names	2022-04-01 11:20:16 -07: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	feat: allow keyword-like projection identifiers	2022-05-10 12:25:30 -07:00