source
opaque Lean.Compiler.LCNF.auxDeclCacheExt :
CacheExtension Decl Name
source
inductive Lean.Compiler.LCNF.CacheAuxDeclResult :
Type

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

Instances For

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

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

Instances For