Documentation
Std
.
Data
.
DTreeMap
.
Raw
.
DecidableEquiv
Search
return to top
source
Imports
Std.Data.DTreeMap.Internal.Lemmas
Std.Data.DTreeMap.Raw.Basic
Imported by
Std
.
DTreeMap
.
Raw
.
instDecidableEquiv
Decidable equivalence for
DTreeMap.Raw
#
source
instance
Std
.
DTreeMap
.
Raw
.
instDecidableEquiv
{
α
:
Type
u}
{
β
:
α
→
Type
v
}
{
cmp
:
α
→
α
→
Ordering
}
[
TransCmp
cmp
]
[
LawfulEqCmp
cmp
]
[
(
k
:
α
) →
BEq
(
β
k
)
]
[
∀ (
k
:
α
),
LawfulBEq
(
β
k
)
]
{
t₁
t₂
:
Raw
α
β
cmp
}
(
h₁
:
t₁
.
WF
)
(
h₂
:
t₂
.
WF
)
:
Decidable
(
t₁
.
Equiv
t₂
)
Equations