Skip to content

Commit 6bb7a12

Browse files
committed
feat: add Heap instances for TreeMap and ExtTreeMap
- Add Store and Heap instances for TreeMap K V cmp - Add Store and Heap instances for ExtTreeMap K V cmp - Add Store, Heap, RepFunStore, IsoFunStore instances for function types - Prove getElem?_mergeWith' with full WF tracking through internal foldl Uses standard library operations (alter, filterMap, mergeWith) directly instead of custom wrappers. Key proof helpers track WF through foldl. Closes #105
1 parent 6138de8 commit 6bb7a12

File tree

2 files changed

+458
-0
lines changed

2 files changed

+458
-0
lines changed

src/Iris/Std.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Iris.Std.Classes
22
import Iris.Std.Expr
3+
import Iris.Std.Heap
4+
import Iris.Std.HeapInstances
35
import Iris.Std.Nat
46
import Iris.Std.Prod
57
import Iris.Std.Qq

0 commit comments

Comments
 (0)