diff options
Diffstat (limited to 'AvlVerification/Tree.lean')
| -rw-r--r-- | AvlVerification/Tree.lean | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean index fdd4b78..8a043a1 100644 --- a/AvlVerification/Tree.lean +++ b/AvlVerification/Tree.lean @@ -75,4 +75,7 @@ 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) +@[simp] +def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry + end Tree |