structure Lean.Compiler.LCNF.BaseTypeExtState : Type

State for the environment extension used to save the LCNF base phase type for declarations that do not have code associated with them. Example: constructors, inductive types, foreign functions.

• base : Lean.PHashMap Lean.Name Lean.Expr

  The LCNF type for the base phase.

instance Lean.Compiler.LCNF.instInhabitedBaseTypeExtState : Inhabited Lean.Compiler.LCNF.BaseTypeExtState

Equations

• Lean.Compiler.LCNF.instInhabitedBaseTypeExtState = { default := { base := default } }

opaque Lean.Compiler.LCNF.baseTypeExt : Lean.EnvExtension Lean.Compiler.LCNF.BaseTypeExtState

def Lean.Compiler.LCNF.getOtherDeclBaseType (declName : Lean.Name) (us : List Lean.Level) : Lean.CoreM Lean.Expr

Equations

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