Dependent tree map lemmas #
This file contains lemmas about Std.Data.DTreeMap.Raw.Basic
. Most of the lemmas require
TransCmp cmp
for the comparison function cmp
and a proof that the involved maps are well-formed.
These proofs can be obtained from Std.Data.DTreeMap.Raw.WF
.
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.
A variant of contains_of_contains_insertMany_list
used in get_insertMany_list
.
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.