instance Lean.Compiler.LCNF.instHashableParam : Hashable Param

Equations

• Lean.Compiler.LCNF.instHashableParam = { hash := fun (p : Lean.Compiler.LCNF.Param) => mixHash (hash p.fvarId) (hash p.type) }

def Lean.Compiler.LCNF.hashParams (ps : Array Param) : UInt64

Equations

• Lean.Compiler.LCNF.hashParams ps = hash ps

partial def Lean.Compiler.LCNF.hashAlt (alt : Alt) : UInt64

partial def Lean.Compiler.LCNF.hashAlts (alts : Array Alt) : UInt64

partial def Lean.Compiler.LCNF.hashCode (code : Code) : UInt64

instance Lean.Compiler.LCNF.instHashableCode : Hashable Code

Equations

• Lean.Compiler.LCNF.instHashableCode = { hash := fun (c : Lean.Compiler.LCNF.Code) => Lean.Compiler.LCNF.hashCode c }

instance Lean.Compiler.LCNF.instHashableDeclValue : Hashable DeclValue

Equations

• Lean.Compiler.LCNF.instHashableDeclValue = { hash := Lean.Compiler.LCNF.hashDeclValue✝ }

instance Lean.Compiler.LCNF.instHashableDecl : Hashable Decl

Equations

• Lean.Compiler.LCNF.instHashableDecl = { hash := Lean.Compiler.LCNF.hashDecl✝ }