Documentation

Lean.ProjFns

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

  • ctorName : 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.

Instances For
    @[export lean_mk_projection_info]
    def Lean.mkProjectionInfoEx (ctorName : Name) (numParams i : Nat) (fromClass : Bool) :
    Equations
      Instances For
        @[export lean_projection_info_from_class]
        Equations
          Instances For
            @[export lean_add_projection_info]
            def Lean.addProjectionFnInfo (env : Environment) (projName ctorName : Name) (numParams i : Nat) (fromClass : Bool) :
            Equations
              Instances For
                @[export lean_get_projection_info]
                Equations
                  Instances For
                    Equations
                      Instances For

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

                        Equations
                          Instances For
                            def Lean.isProjectionFn {m : TypeType} [MonadEnv m] [Monad m] (declName : Name) :
                            Equations
                              Instances For
                                Equations
                                  Instances For