Lean4
/-- Override the Lean 4 pi notation delaborator with one that uses `Π` and prints
cute binders such as `∀ ε > 0`.
Note that this takes advantage of the fact that `(x : α) → p x` notation is
never used for propositions, so we can match on this result and rewrite it. -/
@[scoped delab forallE]
def delabPi' : Delab :=
whenPPOption Lean.getPPNotation
(do
-- Use delabForall as a backup if `pp.mathlib.binderPredicates` is false.
let stx ← delabPi <|> delabForall
let stx : Term ←
match stx with
| `($group:bracketedBinder → $body) =>
`(Π $group:bracketedBinder, $body)
| _ =>
pure stx
match stx with
| `(Π $group, Π $groups*, $body) =>
`(Π $group $groups*, $body)
| _ =>
pure stx)
