Dependent hash map lemmas #
This file contains lemmas about Std.DHashMap
. Most of the lemmas require
EquivBEq α
and LawfulHashable α
for the key type α
. The easiest way to obtain these instances
is to provide an instance of LawfulBEq α
.
This is a restatement of contains_of_contains_insertIfNew
that is written to exactly match the proof
obligation in the statement of get_insertIfNew
.
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.
Equations
Instances For
Equations
Instances For
Simpler variant of get?_filterMap
when LawfulBEq
is available.
Simpler variant of get_filterMap
when LawfulBEq
is available.
Simpler variant of get!_filterMap
when LawfulBEq
is available.
Simpler variant of getD_filterMap
when LawfulBEq
is available.
Simpler variant of get?_filter
when LawfulBEq
is available.
Simpler variant of get!_filter
when LawfulBEq
is available.
Simpler variant of getD_filter
when LawfulBEq
is available.