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
.