opaque Lean.Compiler.LCNF.auxDeclCacheExt : CacheExtension Decl Name

inductive Lean.Compiler.LCNF.CacheAuxDeclResult : Type

• new : CacheAuxDeclResult
• alreadyCached (declName : Name) : CacheAuxDeclResult

def Lean.Compiler.LCNF.cacheAuxDecl (decl : Decl) : CompilerM CacheAuxDeclResult

Equations

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