Dependent hash map lemmas #
This file contains lemmas about Std.Data.DHashMap.Raw
. 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 α
.
Internal implementation detail of the hash map
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.
Instances For
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.