Mathlib-specific pretty printer options.

opaque Mathlib.pp.mathlib.binderPredicates : Lean.Option Bool

The pp.mathlib.binderPredicates option is used to control whether mathlib pretty printers should use binder predicate notation (such as ∀ x < 2, p x).

def Mathlib.getPPBinderPredicates (o : Lean.Options) : Bool

Gets whether pp.mathlib.binderPredicates is enabled.

Equations

• Mathlib.getPPBinderPredicates o = Lean.KVMap.get o Mathlib.pp.mathlib.binderPredicates.name !Lean.getPPAll o