lean4-htt/src/Std/Data/DTreeMap
Kim Morrison 1d5110e140
feat: insertMany_append lemmas for map variants (#8184)
This PR adds the `insertMany_append` lemma for all map variants.
2025-04-30 17:09:51 +00:00
..
Internal feat: unconditional lemmas for HashMap/TreeMap.getElem?_insertMany_list (#8154) 2025-04-30 16:20:41 +00:00
Raw feat: insertMany_append lemmas for map variants (#8184) 2025-04-30 17:09:51 +00:00
AdditionalOperations.lean feat: well-formedness lemmas for raw tree map operations (#7237) 2025-02-27 13:08:41 +00:00
Basic.lean chore: write tests for the non-verified tree map functions (#7680) 2025-03-27 13:52:34 +00:00
Lemmas.lean feat: insertMany_append lemmas for map variants (#8184) 2025-04-30 17:09:51 +00:00
Raw.lean fix: import all raw tree map modules into Std.Data (#8044) 2025-04-24 10:06:32 +00:00