Dependent tree map lemmas #
This file contains lemmas about Std.DTreeMap
. Most of the lemmas require
TransCmp cmp
for the comparison function cmp
.
This is a restatement of mem_of_mem_insertIfNew
that is written to exactly match the
proof obligation in the statement of get_insertIfNew
.
Deprecated, use forMUncurried_eq_forM_toList
together with forM_eq_forMUncurried
instead.
Deprecated, use forInUncurried_eq_forIn_toList
together with forIn_eq_forInUncurried
instead.
Implementation detail of the tree map
Equations
- Std.DTreeMap.isSetoid α β cmp = { r := Std.DTreeMap.Equiv, iseqv := ⋯ }
Instances For
Simpler variant of get?_filterMap
when LawfulEqCmp
is available.
Simpler variant of get_filterMap
when LawfulEqCmp
is available.
Simpler variant of get!_filterMap
when LawfulEqCmp
is available.
Simpler variant of getD_filterMap
when LawfulEqCmp
is available.
Simpler variant of get?_filter
when LawfulEqCmp
is available.
Simpler variant of get!_filter
when LawfulEqCmp
is available.
Simpler variant of getD_filter
when LawfulEqCmp
is available.