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.