Make progress on updating the proofs of the AVL trees

AeneasVerif · Jul 4, 2024 · 5f0e848 · 5f0e848
1 parent 0305ad9
commit 5f0e848
Show file tree

Hide file tree

Showing 11 changed files with 328 additions and 471 deletions.
diff --git a/tests/lean/Avl/AVL.lean b/tests/lean/Avl/AVL.lean
diff --git a/tests/lean/Avl/BinarySearchTree.lean b/tests/lean/Avl/BinarySearchTree.lean
diff --git a/tests/lean/Avl/Find.lean b/tests/lean/Avl/Find.lean
@@ -2,7 +2,7 @@ import Avl.Tree
 import Avl.BinarySearchTree
 import Avl.Specifications
 
-namespace Implementation
+namespace avl
 
 open Primitives
 open avl
@@ -43,4 +43,4 @@ def AVLTreeSet.find_spec
     rw [AVLTreeSet.find]
     progress; simp only [Result.ok.injEq, exists_eq_left']; assumption
 
-end Implementation
+end avl