lean4-htt/src/Std/Data
Paul Reichert 60a9f8e492
feat: well-formedness lemmas for raw tree map operations (#7237)
This PR provides proofs that the raw tree map operations are well-formed
and refactors the file structure of the tree map, introducing new
modules `Std.{DTreeMap,TreeMap,TreeSet}.Raw` and splittting
`AdditionalOperations` into separate files for bundled and raw types.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
2025-02-27 13:08:41 +00:00
..
DHashMap feat: align lemmas about List.getLast(!?) with Array/Vector.back(!?) (#7205) 2025-02-24 11:48:43 +00:00
DTreeMap feat: well-formedness lemmas for raw tree map operations (#7237) 2025-02-27 13:08:41 +00:00
HashMap feat: TreeMap lemmas for 'get?' (#7167) 2025-02-24 15:34:37 +00:00
HashSet feat: verify fold/for variants for Hashmaps (#7137) 2025-02-21 16:08:33 +00:00
Internal feat: verify fold/for variants for Hashmaps (#7137) 2025-02-21 16:08:33 +00:00
TreeMap feat: well-formedness lemmas for raw tree map operations (#7237) 2025-02-27 13:08:41 +00:00
TreeSet feat: well-formedness lemmas for raw tree map operations (#7237) 2025-02-27 13:08:41 +00:00
DHashMap.lean fix: unorphan modules in Std.Data (#4679) 2024-07-08 07:57:56 +00:00
DTreeMap.lean feat: tree map data structures and operations (#6914) 2025-02-11 14:47:47 +00:00
HashMap.lean feat: Std.HashMap (#4583) 2024-07-05 10:14:20 +00:00
HashSet.lean feat: Std.HashMap (#4583) 2024-07-05 10:14:20 +00:00
TreeMap.lean feat: tree map data structures and operations (#6914) 2025-02-11 14:47:47 +00:00
TreeSet.lean feat: min, max, minKey, maxKey, atIndex, getEntryLE, getKeyLE, ... functions for the tree map (#7070) 2025-02-17 14:00:42 +00:00