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.