structure Lean.ProjectionFunctionInfo : Type

• Constructor associated with the auxiliary projection function.

  ctorName : Lean.Name

• Number of parameters in the structure

  numParams : Nat

• The field index associated with the auxiliary projection function.

  i : Nat

• true if the structure is a class.

  fromClass : Bool

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

Equations

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

@[export lean_mk_projection_info]

def Lean.mkProjectionInfoEx (ctorName : Lean.Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Lean.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 : Lean.ProjectionFunctionInfo) : Bool

Equations

• Lean.ProjectionFunctionInfo.fromClassEx info = info.fromClass

opaque Lean.projectionFnInfoExt : Lean.MapDeclarationExtension Lean.ProjectionFunctionInfo

@[export lean_add_projection_info]

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

Equations

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

@[export lean_get_projection_info]

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

Equations

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

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

Equations

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

def Lean.Environment.getProjectionStructureName? (env : Lean.Environment) (projName : Lean.Name) : Option Lean.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} [inst : Lean.MonadEnv m] [inst : Monad m] (declName : Lean.Name) : m Bool

Equations

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

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

Equations

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