summaryrefslogtreecommitdiff
path: root/tests/lean/misc-external/lakefile.lean
diff options
context:
space:
mode:
authorSon HO2023-07-31 16:15:58 +0200
committerGitHub2023-07-31 16:15:58 +0200
commit887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch)
tree92d6021eb549f7cc25501856edd58859786b7e90 /tests/lean/misc-external/lakefile.lean
parent53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff)
parent9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff)
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to '')
-rw-r--r--tests/lean/misc-external/lakefile.lean12
1 files changed, 0 insertions, 12 deletions
diff --git a/tests/lean/misc-external/lakefile.lean b/tests/lean/misc-external/lakefile.lean
deleted file mode 100644
index 6cc4aae4..00000000
--- a/tests/lean/misc-external/lakefile.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Lake
-open Lake DSL
-
-require mathlib from git
- "https://github.com/leanprover-community/mathlib4.git"
-
-package «external» {}
-
-lean_lib «Base» {}
-
-@[default_target]
-lean_lib «External» {}