opaque Lean.Compiler.LCNF.baseTypeExt : CacheExtension Name Expr

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.

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.