Documentation

Lean.ProjFns

structure Lean.ProjectionFunctionInfo :

Type

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

instance Lean.instInhabitedProjectionFunctionInfo :

Inhabited Lean.ProjectionFunctionInfo

Equations

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

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 }

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

Equations

Lean.ProjectionFunctionInfo.fromClassEx info = info.fromClass

constant Lean.projectionFnInfoExt :

Lean.MapDeclarationExtension Lean.ProjectionFunctionInfo

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

Lean.Environment

Equations

Lean.addProjectionFnInfo env projName ctorName numParams i fromClass = Lean.MapDeclarationExtension.insert Lean.projectionFnInfoExt env projName { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass }

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) :

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

Equations

Lean.Environment.getProjectionStructureName? env projName = match Lean.Environment.getProjectionFnInfo? env projName with | none => none | some projInfo => match Lean.Environment.find? env projInfo.ctorName with | some (Lean.ConstantInfo.ctorInfo val) => some val.induct | x => none

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

Equations

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