structure Lean.ProjectionFunctionInfo : Type

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

instance Lean.instInhabitedProjectionFunctionInfo : Inhabited Lean.ProjectionFunctionInfo

@[export lean_mk_projection_info]

def Lean.mkProjectionInfoEx (ctorName : Lake.Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Lean.ProjectionFunctionInfo

@[export lean_projection_info_from_class]

def Lean.ProjectionFunctionInfo.fromClassEx (info : Lean.ProjectionFunctionInfo) : Bool

opaque Lean.projectionFnInfoExt : Lean.MapDeclarationExtension Lean.ProjectionFunctionInfo

@[export lean_add_projection_info]

def Lean.addProjectionFnInfo (env : Lean.Environment) (projName : Lake.Name) (ctorName : Lake.Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Lean.Environment

@[export lean_get_projection_info]

def Lean.Environment.getProjectionFnInfo? (env : Lean.Environment) (projName : Lake.Name) : Option Lean.ProjectionFunctionInfo

def Lean.Environment.isProjectionFn (env : Lean.Environment) (declName : Lake.Name) : Bool

def Lean.Environment.getProjectionStructureName? (env : Lean.Environment) (projName : Lake.Name) : Option Lake.Name

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

def Lean.isProjectionFn {m : Type → Type} [Lean.MonadEnv m] [Monad m] (declName : Lake.Name) : m Bool

def Lean.getProjectionFnInfo? {m : Type → Type} [Lean.MonadEnv m] [Monad m] (declName : Lake.Name) : m (Option Lean.ProjectionFunctionInfo)