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 α.
Instances For
Instances For
Instances For
Equations
Instances For
Equations
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.
Internal implementation detail of the hash map.
Equations
- Std.DHashMap.isSetoid α β = { r := Std.DHashMap.Equiv, iseqv := ⋯ }
Instances For
Instances For
Instances For
Simpler variant of getD_filter when LawfulBEq is available.