diff options
| author | Raito Bezarius | 2024-04-12 19:11:16 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-12 19:11:16 +0200 |
| commit | 3577c7dc9d3013d401c45a7628b0ff4b6fd0ec67 (patch) | |
| tree | 6d481e2bb1ffa6ced38cde52efa09aa2dbda1889 /AvlVerification/Tree.lean | |
| parent | 50be416e22a39eaf59f7edba81b919e1f114a0ae (diff) | |
feat: upgrade and close all proofs except Preorder on U32
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to 'AvlVerification/Tree.lean')
| -rw-r--r-- | AvlVerification/Tree.lean | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean index 3316e9e..fdd4b78 100644 --- a/AvlVerification/Tree.lean +++ b/AvlVerification/Tree.lean @@ -75,7 +75,4 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode. def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t) -def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry -def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry - end Tree |