structure Lean.Compiler.LCNF.BaseTypeExtState : Type

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

  The LCNF type for the base phase.

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.

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

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

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