# Functions for analyzing projections for pretty printing #

source
def Lean.PrettyPrinter.Delaborator.fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) :
MetaM (Option (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.

Instances For

source
def Lean.PrettyPrinter.Delaborator.parentProj? (explicit : Bool) (e : Expr) :
MetaM (Option 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.

Instances For

source
def Lean.PrettyPrinter.Delaborator.isParentProj (explicit : Bool) (e : Expr) :
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

Instances For