@[reducible, inline]

abbrev Lean.Compiler.LCNF.AuxDeclCache : Type

Equations

• Lean.Compiler.LCNF.AuxDeclCache = Lean.PHashMap Lean.Compiler.LCNF.Decl Lean.Name

opaque Lean.Compiler.LCNF.auxDeclCacheExt : EnvExtension AuxDeclCache

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.