lean4-htt/src/Std/Data/HashMap
Kim Morrison 6e2e1a4f89
chore: consistently add @[simp] to getKey_eq map lemmas (#8186)
These lemmas were inconsistently marked as `@[simp]`, but they seem
generally useful, so this uniformly marks this lemmas as `@[simp]` for
all map variants.
2025-05-03 16:12:33 +00:00
..
AdditionalOperations.lean feat: hash map lemmas for filter, map and filterMap (#7400) 2025-04-17 10:15:52 +00:00
Basic.lean feat: extensional hash maps (#8004) 2025-04-28 06:48:25 +00:00
Lemmas.lean chore: consistently add @[simp] to getKey_eq map lemmas (#8186) 2025-05-03 16:12:33 +00:00
Raw.lean feat: extensional hash maps (#8004) 2025-04-28 06:48:25 +00:00
RawLemmas.lean chore: consistently add @[simp] to getKey_eq map lemmas (#8186) 2025-05-03 16:12:33 +00:00