lean4-htt/src/Std/Data/TreeMap
Kim Morrison 34d944c4a9
feat: add ofList_eq_insertMany_empty lemmas for map types (#8182)
This PR adds `ofList_eq_insertMany_empty` lemmas for all the hash/tree
map types, with the exception of
`Std.HashSet.Raw.ofList_eq_insertMany_empty`.
2025-05-02 17:16:23 +00:00
..
Raw feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +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: fix TreeMap deprecations (#8100) 2025-04-26 13:10:05 +00:00
Lemmas.lean feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
Raw.lean fix: import all raw tree map modules into Std.Data (#8044) 2025-04-24 10:06:32 +00:00