Documentation

Lean.Compiler.LCNF.DeclHash

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashableParam {pu : Purity} :

Hashable (Param pu)

Equations

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

def Lean.Compiler.LCNF.hashParams {pu : Purity} (ps : Array (Param pu)) :

Equations

Lean.Compiler.LCNF.hashParams ps = hash ps

Instances For

partial def Lean.Compiler.LCNF.hashAlt {pu : Purity} (alt : Alt pu) :

partial def Lean.Compiler.LCNF.hashAlts {pu : Purity} (alts : Array (Alt pu)) :

partial def Lean.Compiler.LCNF.hashCode {pu : Purity} (code : Code pu) :

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashableCode {pu : Purity} :

Hashable (Code pu)

Equations

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

def Lean.Compiler.LCNF.instHashableDeclValue.hash {pu✝ : Purity} :

DeclValue pu✝ → UInt64

Equations

Instances For

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashableDeclValue {pu✝ : Purity} :

Hashable (DeclValue pu✝)

Equations

Lean.Compiler.LCNF.instHashableDeclValue = { hash := Lean.Compiler.LCNF.instHashableDeclValue.hash }

def Lean.Compiler.LCNF.instHashableSignature.hash {pu✝ : Purity} :

Signature pu✝ → UInt64

Equations

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

Instances For

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashableSignature {pu✝ : Purity} :

Hashable (Signature pu✝)

Equations

Lean.Compiler.LCNF.instHashableSignature = { hash := Lean.Compiler.LCNF.instHashableSignature.hash }

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashableDecl {pu✝ : Purity} :

Hashable (Decl pu✝)

Equations

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

def Lean.Compiler.LCNF.instHashableDecl.hash {pu✝ : Purity} :

Decl pu✝ → UInt64

Equations

Lean.Compiler.LCNF.instHashableDecl.hash { toSignature := a, value := a_1, recursive := a_2, inlineAttr? := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

Instances For