Lean.ProjFns

source

structure Lean.ProjectionFunctionInfo:

Type

ctorName : Lean.Name
numParams : Nat
i : Nat
fromClass : Bool

source

instance Lean.instInhabitedProjectionFunctionInfo:

Inhabited Lean.ProjectionFunctionInfo

Equations

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

source

@[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 }

source

@[export lean_projection_info_from_class]

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

Bool

Equations

Lean.ProjectionFunctionInfo.fromClassEx info = info.fromClass

source

opaque Lean.projectionFnInfoExt:

Lean.MapDeclarationExtension Lean.ProjectionFunctionInfo

source

@[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.

source

@[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

source

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

Bool

Equations

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

source

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.

source

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

m Bool

Equations

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

source

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 a ← Lean.getEnv pure (Lean.Environment.getProjectionFnInfo? a declName)