summaryrefslogtreecommitdiff
path: root/tests/lean/misc-loops
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/misc-loops/Loops.lean1
-rw-r--r--tests/lean/misc-loops/lake-manifest.json27
-rw-r--r--tests/lean/misc-loops/lakefile.lean14
-rw-r--r--tests/lean/misc-loops/lean-toolchain1
4 files changed, 33 insertions, 10 deletions
diff --git a/tests/lean/misc-loops/Loops.lean b/tests/lean/misc-loops/Loops.lean
new file mode 100644
index 00000000..60c73776
--- /dev/null
+++ b/tests/lean/misc-loops/Loops.lean
@@ -0,0 +1 @@
+import Loops.Funs
diff --git a/tests/lean/misc-loops/lake-manifest.json b/tests/lean/misc-loops/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-loops/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-loops/lakefile.lean b/tests/lean/misc-loops/lakefile.lean
index 0d20ba1f..097c0a7d 100644
--- a/tests/lean/misc-loops/lakefile.lean
+++ b/tests/lean/misc-loops/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «loops» {
- -- add package configuration options here
-}
+package «loops» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «Loops» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «Loops» {}
diff --git a/tests/lean/misc-loops/lean-toolchain b/tests/lean/misc-loops/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-loops/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21