lean4-htt/src/Lean/PrettyPrinter
2022-07-09 15:24:22 -07:00
..
Delaborator refactor: prepare to elaborate a[i] notation using typeclasses 2022-07-09 15:24:22 -07:00
Basic.lean chore: throwError! => throwError, throwErrorAt! => throwErrorAt 2021-03-11 11:59:45 -08:00
Delaborator.lean refactor: pp.analyze needs pp options 2021-08-03 09:13:18 +02:00
Formatter.lean fix: store syntax kinds of parser aliases in order to construct correct antiquotations in macro and elab 2022-06-27 22:37:02 +02:00
Parenthesizer.lean fix: backtrack on unexpected non-identifier in parenthesizer 2022-07-08 14:49:08 +02:00