Documentation
Lean
.
Compiler
.
LCNF
.
DeclHash
Search
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✝
}