structure Lean.ProjectionFunctionInfo : Type

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.

@[implicit_reducible]

instance Lean.instInhabitedProjectionFunctionInfo : Inhabited ProjectionFunctionInfo

Equations

• Lean.instInhabitedProjectionFunctionInfo = { default := Lean.instInhabitedProjectionFunctionInfo.default }

def Lean.instInhabitedProjectionFunctionInfo.default : ProjectionFunctionInfo

Equations

• Lean.instInhabitedProjectionFunctionInfo.default = { ctorName := default, numParams := default, i := default, fromClass := default }

def Lean.instReprProjectionFunctionInfo.repr : ProjectionFunctionInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.instReprProjectionFunctionInfo : Repr ProjectionFunctionInfo

Equations

• Lean.instReprProjectionFunctionInfo = { reprPrec := Lean.instReprProjectionFunctionInfo.repr }

@[export lean_mk_projection_info]

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

Equations

• Lean.mkProjectionInfoEx ctorName numParams i fromClass = { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass }

@[export lean_projection_info_from_class]

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

Equations

• info.fromClassEx = info.fromClass

opaque Lean.projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• env.getProjectionFnInfo? projName = Lean.projectionFnInfoExt.find? env projName

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

Equations

• env.isProjectionFn declName = Lean.projectionFnInfoExt.contains env declName

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

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.

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

Equations

• Lean.isProjectionFn declName = do let __do_lift ← Lean.getEnv pure (__do_lift.isProjectionFn declName)

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

Equations

• Lean.getProjectionFnInfo? declName = do let __do_lift ← Lean.getEnv pure (__do_lift.getProjectionFnInfo? declName)

structure Lean.AuxParentProjectionInfo : Type

Auxiliary parent projection created when a parent structure cannot be represented as a subobject (e.g., due to diamond inheritance). Unlike regular projections, these construct the parent value from individual fields rather than extracting a single field. Example: AddMonoid'.toAddZero' when AddZero' cannot be a subobject of AddMonoid'.

• numParams : Nat

  Number of parameters in the child structure.

• fromClass : Bool

  true if the child structure is a class.

def Lean.instInhabitedAuxParentProjectionInfo.default : AuxParentProjectionInfo

Equations

• Lean.instInhabitedAuxParentProjectionInfo.default = { numParams := default, fromClass := default }

@[implicit_reducible]

instance Lean.instInhabitedAuxParentProjectionInfo : Inhabited AuxParentProjectionInfo

Equations

• Lean.instInhabitedAuxParentProjectionInfo = { default := Lean.instInhabitedAuxParentProjectionInfo.default }

@[implicit_reducible]

instance Lean.instReprAuxParentProjectionInfo : Repr AuxParentProjectionInfo

Equations

• Lean.instReprAuxParentProjectionInfo = { reprPrec := Lean.instReprAuxParentProjectionInfo.repr }

def Lean.instReprAuxParentProjectionInfo.repr : AuxParentProjectionInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo

def Lean.addAuxParentProjectionInfo (env : Environment) (projName : Name) (numParams : Nat) (fromClass : Bool) : Environment

Equations

• Lean.addAuxParentProjectionInfo env projName numParams fromClass = Lean.auxParentProjInfoExt.insert env projName { numParams := numParams, fromClass := fromClass }

def Lean.Environment.getAuxParentProjectionInfo? (env : Environment) (projName : Name) : Option AuxParentProjectionInfo

Equations

• env.getAuxParentProjectionInfo? projName = Lean.auxParentProjInfoExt.find? env projName

def Lean.getAuxParentProjectionInfo? {m : Type → Type} [MonadEnv m] [Monad m] (declName : Name) : m (Option AuxParentProjectionInfo)

Equations

• Lean.getAuxParentProjectionInfo? declName = do let __do_lift ← Lean.getEnv pure (__do_lift.getAuxParentProjectionInfo? declName)