Documentation

Lean.PrettyPrinter.Delaborator.FieldNotation

Functions for analyzing projections for pretty printing #

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