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 : PHashMap Name Expr

  The LCNF type for the base phase.

instance Lean.Compiler.LCNF.instInhabitedBaseTypeExtState : Inhabited BaseTypeExtState

Equations

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

opaque Lean.Compiler.LCNF.baseTypeExt : EnvExtension BaseTypeExtState

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

Equations

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