Documentation
Lean.Compiler.LCNF.DeclHash
Google site search
Lean.Compiler.LCNF.DeclHash
source
Imports
Init
Lean.Compiler.LCNF.Basic
Imported by
Lean.Compiler.LCNF.instHashableParam
Lean.Compiler.LCNF.hashParams
Lean.Compiler.LCNF.hashAlt
Lean.Compiler.LCNF.hashAlts
Lean.Compiler.LCNF.hashCode
Lean.Compiler.LCNF.instHashableCode
Lean.Compiler.LCNF.instHashableDecl
source
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
)
}
source
def
Lean.Compiler.LCNF.hashParams
(ps :
Array
Lean.Compiler.LCNF.Param
)
:
UInt64
Equations
Lean.Compiler.LCNF.hashParams
ps
=
hash
ps
source
partial def
Lean.Compiler.LCNF.hashAlt
(alt :
Lean.Compiler.LCNF.Alt
)
:
UInt64
source
partial def
Lean.Compiler.LCNF.hashAlts
(alts :
Array
Lean.Compiler.LCNF.Alt
)
:
UInt64
source
partial def
Lean.Compiler.LCNF.hashCode
(code :
Lean.Compiler.LCNF.Code
)
:
UInt64
source
instance
Lean.Compiler.LCNF.instHashableCode
:
Hashable
Lean.Compiler.LCNF.Code
Equations
Lean.Compiler.LCNF.instHashableCode
=
{
hash
:=
fun
c
=>
Lean.Compiler.LCNF.hashCode
c
}
source
instance
Lean.Compiler.LCNF.instHashableDecl
:
Hashable
Lean.Compiler.LCNF.Decl
Equations
Lean.Compiler.LCNF.instHashableDecl
=
{
hash
:=
Lean.Compiler.LCNF.hashDecl✝
}