Documentation

Lean.PrettyPrinter.Delaborator.FieldNotation

Functions for analyzing projections for pretty printing #

def Lean.PrettyPrinter.Delaborator.fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) :

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.

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.

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