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>
---
 lakefile.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lakefile.lean')

diff --git a/lakefile.lean b/lakefile.lean
index ccc0a55..743a0db 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,9 +4,9 @@ open Lake DSL
 require base from git
   "https://github.com/AeneasVerif/aeneas"@"main"/"backends/lean"
 
-package «AvlVerification» where
+package «Verification» where
   -- add package configuration options here
 
 @[default_target]
-lean_lib «AvlVerification» where
+lean_lib «Verification» where
   -- add library configuration options here
-- 
cgit v1.2.3

