summaryrefslogtreecommitdiff
path: root/lakefile.lean
diff options
context:
space:
mode:
authorRaito Bezarius2024-04-12 20:05:13 +0200
committerRaito Bezarius2024-04-12 20:05:13 +0200
commit4af0e431f4201e20308a8f7472bf7262e2f7b1a2 (patch)
tree5f1898bd9017de0b3b097b60bc2893152b979a1b /lakefile.lean
parent71d7e8af74c052d671968696fdb70cede5b78d8a (diff)
feat: upgrade to lean v4.7
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to 'lakefile.lean')
-rw-r--r--lakefile.lean9
1 files changed, 1 insertions, 8 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