@[inline, reducible]

abbrev Lean.Compiler.LCNF.AuxDeclCache : Type

Equations

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

opaque Lean.Compiler.LCNF.auxDeclCacheExt : Lean.EnvExtension Lean.Compiler.LCNF.AuxDeclCache

inductive Lean.Compiler.LCNF.CacheAuxDeclResult : Type

• new: Lean.Compiler.LCNF.CacheAuxDeclResult
• alreadyCached: Lake.Name → Lean.Compiler.LCNF.CacheAuxDeclResult

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

Equations

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