lean4-htt/src/Lean/PrettyPrinter
Kyle Miller 76a7754d08 fix: have parenthesizer copy source info to parenthesized term
This causes the info view to have the entire parenthesized expression be hoverable.
2023-11-14 20:24:30 +01:00
..
Delaborator feat: check task cancellation in elaborator 2023-10-26 08:33:09 +02:00
Basic.lean chore: import reductions 2022-09-15 14:02:38 -07:00
Delaborator.lean refactor: pp.analyze needs pp options 2021-08-03 09:13:18 +02:00
Formatter.lean feat: hygieneInfo parser (aka this 2.0) 2023-06-02 16:19:02 +02:00
Parenthesizer.lean fix: have parenthesizer copy source info to parenthesized term 2023-11-14 20:24:30 +01:00