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.

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.

    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.

      Instances For