max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Std/Data/TreeMap
History
Paul Reichert c934e6c247
feat: tree map lemmas about containsThenInsert(IfNew) (#7165) 
This PR provides tree map lemmas about the interaction of
`containsThenInsert(IfNew)` with `contains` and `insert(IfNew)`.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
2025-02-24 09:01:45 +00:00
..
AdditionalOperations.lean feat: min, max, minKey, maxKey, atIndex, getEntryLE, getKeyLE, ... functions for the tree map (#7070) 2025-02-17 14:00:42 +00:00
Basic.lean feat: modify and alter functions for the tree map (#7118) 2025-02-20 09:50:10 +00:00
Lemmas.lean feat: tree map lemmas about containsThenInsert(IfNew) (#7165) 2025-02-24 09:01:45 +00:00
Raw.lean feat: modify and alter functions for the tree map (#7118) 2025-02-20 09:50:10 +00:00
RawLemmas.lean feat: tree map lemmas about containsThenInsert(IfNew) (#7165) 2025-02-24 09:01:45 +00:00