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