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 --- 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