Documentation
Std
.
Data
.
DHashMap
.
DecidableEquiv
Search
return to top
source
Imports
Std.Data.DHashMap.Internal.RawLemmas
Imported by
Std
.
DHashMap
.
instDecidableEquivOfLawfulBEq
Decidable equivalence for
DHashMap
#
source
instance
Std
.
DHashMap
.
instDecidableEquivOfLawfulBEq
{
α
:
Type
u}
{
β
:
α
→
Type
v
}
[
BEq
α
]
[
LawfulBEq
α
]
[
Hashable
α
]
[
(
k
:
α
) →
BEq
(
β
k
)
]
[
∀ (
k
:
α
),
LawfulBEq
(
β
k
)
]
(
m₁
m₂
:
DHashMap
α
β
)
:
Decidable
(
m₁
.
Equiv
m₂
)
Equations