summaryrefslogtreecommitdiff
path: root/AvlVerification/Tree.lean
diff options
context:
space:
mode:
Diffstat (limited to 'AvlVerification/Tree.lean')
-rw-r--r--AvlVerification/Tree.lean3
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