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>
---
 Verification.lean | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Verification.lean

(limited to 'Verification.lean')

diff --git a/Verification.lean b/Verification.lean
new file mode 100644
index 0000000..31d8103
--- /dev/null
+++ b/Verification.lean
@@ -0,0 +1,2 @@
+import Verification.Insert
+import Verification.Find
-- 
cgit v1.2.3