Documentation

Lean.PrettyPrinter.Delaborator.FieldNotation

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.
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.
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