Documentation

Lean.Compiler.LCNF.DeclHash

instance Lean.Compiler.LCNF.instHashableParam :

Hashable Lean.Compiler.LCNF.Param

Equations

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

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

Equations

Lean.Compiler.LCNF.hashParams ps = hash ps

Instances For

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

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

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

instance Lean.Compiler.LCNF.instHashableCode :

Hashable Lean.Compiler.LCNF.Code

Equations

Lean.Compiler.LCNF.instHashableCode = { hash := fun c => Lean.Compiler.LCNF.hashCode c }

instance Lean.Compiler.LCNF.instHashableDecl :

Hashable Lean.Compiler.LCNF.Decl

Equations

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