Functions for analyzing projections for pretty printing

def Lean.PrettyPrinter.Delaborator.fieldNotationCandidate? (f : Lean.Expr) (args : Array Lean.Expr) (useGeneralizedFieldNotation : Bool) : Lean.MetaM (Option (Lake.Name × Nat))

If f is a function that can be used for field notation, returns the field name to use and the argument index for the object of the field notation.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Delaborator.parentProj? (explicit : Bool) (e : Lean.Expr) : Lean.MetaM (Option Lake.Name)

Returns the field name of the projection if e is an application that is a projection to a parent structure. If explicit is true, then requires that the structure have no parameters.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Delaborator.isParentProj (explicit : Bool) (e : Lean.Expr) : Lean.MetaM Bool

Returns true if e is an application that is a projection to a parent structure. If explicit is true, then requires that the structure have no parameters.

Equations

• Lean.PrettyPrinter.Delaborator.isParentProj explicit e = do let __do_lift ← Lean.PrettyPrinter.Delaborator.parentProj? explicit e pure __do_lift.isSome