Kyle Miller a706c3b89a feat: delaboration collapses parent projections (#3326) ... When projection functions are delaborated, intermediate parent projections are no longer printed. For example, rather than pretty printing as `o.toB.toA.x` with these `toB` and `toA` parent projections, it pretty prints as `o.x`. This feature is being upstreamed from mathlib.		2024-02-14 23:44:48 +00:00
..
Basic.lean	feat: elidible subterms (#3201)	2024-01-31 17:28:29 +00:00
Builtins.lean	feat: delaboration collapses parent projections (#3326)	2024-02-14 23:44:48 +00:00
Options.lean	feat: pp.numericTypes option for printing number literals with type ascriptions (#2933)	2024-02-01 17:23:32 +11:00
SubExpr.lean	feat: extract delabAppCore, define withOverApp, and make over-applied projections pretty print (#3083)	2024-01-10 13:24:28 +00:00
TopDownAnalyze.lean	feat: check task cancellation in elaborator	2023-10-26 08:33:09 +02:00