structure Lean.Compiler.LCNF.AuxDeclCacheKey : Type

• pu : Purity
• decl : Decl self.pu

def Lean.Compiler.LCNF.instBEqAuxDeclCacheKey.beq : AuxDeclCacheKey → AuxDeclCacheKey → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.instBEqAuxDeclCacheKey.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqAuxDeclCacheKey : BEq AuxDeclCacheKey

Equations

• Lean.Compiler.LCNF.instBEqAuxDeclCacheKey = { beq := Lean.Compiler.LCNF.instBEqAuxDeclCacheKey.beq }

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashableAuxDeclCacheKey : Hashable AuxDeclCacheKey

Equations

• Lean.Compiler.LCNF.instHashableAuxDeclCacheKey = { hash := Lean.Compiler.LCNF.instHashableAuxDeclCacheKey.hash }

def Lean.Compiler.LCNF.instHashableAuxDeclCacheKey.hash : AuxDeclCacheKey → UInt64

Equations

• Lean.Compiler.LCNF.instHashableAuxDeclCacheKey.hash { pu := a, decl := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

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

inductive Lean.Compiler.LCNF.CacheAuxDeclResult : Type

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

def Lean.Compiler.LCNF.cacheAuxDecl {pu : Purity} (decl : Decl pu) : CompilerM CacheAuxDeclResult

Equations

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