source
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.

source
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.

Instances For