From 4af0e431f4201e20308a8f7472bf7262e2f7b1a2 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Fri, 12 Apr 2024 20:05:13 +0200
Subject: feat: upgrade to lean v4.7

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 lakefile.lean  | 9 +--------
 lean-toolchain | 2 +-
 2 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index f92b653..ccc0a55 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,13 +7,6 @@ require base from git
 package «AvlVerification» where
   -- add package configuration options here
 
+@[default_target]
 lean_lib «AvlVerification» where
   -- add library configuration options here
-
-@[default_target]
-lean_exe «avlverification» where
-  root := `Main
-  -- Enables the use of the Lean interpreter by the executable (e.g.,
-  -- `runFrontend`) at the expense of increased binary size on Linux.
-  -- Remove this line if you do not need such functionality.
-  supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
index cfcdd32..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.7.0
-- 
cgit v1.2.3