Documentation

Lean.ProjFns

  • ctorName : Lake.Name

    Constructor associated with the auxiliary projection function.

  • numParams : Nat

    Number of parameters in the structure

  • i : Nat

    The field index associated with the auxiliary projection function.

  • fromClass : Bool

    true if the structure is a class.

Given a structure S, Lean automatically creates an auxiliary definition (projection function) for each field. This structure caches information about these auxiliary definitions.

Instances For
Equations
@[export lean_mk_projection_info]
def Lean.mkProjectionInfoEx (ctorName : Lake.Name) (numParams : Nat) (i : Nat) (fromClass : Bool) :
Equations
  • Lean.mkProjectionInfoEx ctorName numParams i fromClass = { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass }
Instances For
    @[export lean_projection_info_from_class]
    Equations
    Instances For
      @[export lean_add_projection_info]
      def Lean.addProjectionFnInfo (env : Lean.Environment) (projName : Lake.Name) (ctorName : Lake.Name) (numParams : Nat) (i : Nat) (fromClass : Bool) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        If projName is the name of a projection function, return the associated structure name

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.isProjectionFn {m : TypeType} [Lean.MonadEnv m] [Monad m] (declName : Lake.Name) :
          Equations
          Instances For
            Equations
            Instances For