From 945c630ec18e282bd0db731fb3f0b521e99de059 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Wed, 17 Apr 2024 15:08:07 +0200
Subject: feat: add functional correctness of elements contained in the
 resulting tree

We revamp the typeclass mechanisms and we add an equality hypothesis
now.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Tree.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'AvlVerification/Tree.lean')

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
-- 
cgit v1.2.3

