From b650710ad3f8c14b713bdf52f684f472115dce2f Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Tue, 23 Apr 2024 14:24:04 +0200
Subject: feat: close `find` / `insert` proofs

After a complete 180 with the Order theory, we close the goals of find
and insert and we give an example of U32 order that we will upstream to
Aeneas directly.

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

(limited to 'AvlVerification.lean')

diff --git a/AvlVerification.lean b/AvlVerification.lean
index 9380768..fee58d5 100644
--- a/AvlVerification.lean
+++ b/AvlVerification.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [avl_verification]
 import Base
+
 open Primitives
 
 namespace avl_verification
@@ -93,8 +94,8 @@ def AVLTreeSet.insert
   Result (Bool × (AVLTreeSet T))
   :=
   do
-  let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root
-  Result.ok (b, { root := as })
+  let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root
+  Result.ok (b, { root := u })
 
 /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
    Source: 'src/main.rs', lines 65:4-65:43 -/
-- 
cgit v1.2.3