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
    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
        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
            Instances For