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

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 : Lake.Name) (us : List Lean.Level) : Lean.CoreM Lean.Expr

Equations

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