Daniel Selsam 3309da8f1e fix: pp.analyze LocalInstances not in MessageData		2021-08-03 09:13:18 +02:00
..
Basic.lean	feat: pp option to instantiate mvars	2021-08-03 09:13:18 +02:00
Builtins.lean	feat: turn more delaborators into unexpanders	2021-08-03 09:13:18 +02:00
SubExpr.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
TopDownAnalyze.lean	fix: pp.analyze LocalInstances not in MessageData	2021-08-03 09:13:18 +02:00