Commit 2023-11-24 03:30 c26fbb12

View on Github →

feat: analysis delaborator for LinearIndependent (#8602) This is an experimental delaborator that works by analyzing the expression and tagging it with pp.analysis-style hints. This causes pretty printing LinearIndependent like LinearIndependent K fun (b : ↑s) ↦ ↑b rather than LinearIndependent K fun b ↦ ↑b and LinearIndependent (ι := { x // x ∈ s }) K Subtype.val rather than LinearIndependent K Subtype.val.

Estimated changes