summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-02-02 23:17:30 +0100
committerSon Ho2024-02-02 23:17:30 +0100
commit5cf7d9c0d6b0bc77f2219e7b8b29badce26d51e8 (patch)
treec0b07a0b4c3d03787cdece5d6ab6d06311bd17db /tests
parent63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 (diff)
Make progress on fixing the tests
Diffstat (limited to 'tests')
-rw-r--r--tests/lean/lakefile.lean26
1 files changed, 13 insertions, 13 deletions
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index fef94971..502d8098 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -4,19 +4,19 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-require Base from "../../backends/lean"
+require base from "../../backends/lean"
-package «tests» {}
+package «Tests» {}
-@[default_target] lean_lib tutorial
-@[default_target] lean_lib betreeMain
-@[default_target] lean_lib constants
-@[default_target] lean_lib external
-@[default_target] lean_lib hashmap
-@[default_target] lean_lib hashmapMain
-@[default_target] lean_lib loops
-@[default_target] lean_lib noNestedBorrows
-@[default_target] lean_lib paper
-@[default_target] lean_lib poloniusList
@[default_target] lean_lib array
-@[default_target] lean_lib traits
+@[default_target] lean_lib Tutorial
+@[default_target] lean_lib BetreeMain
+@[default_target] lean_lib Constants
+@[default_target] lean_lib External
+@[default_target] lean_lib Hashmap
+@[default_target] lean_lib HashmapMain
+@[default_target] lean_lib Loops
+@[default_target] lean_lib NoNestedBorrows
+@[default_target] lean_lib Paper
+@[default_target] lean_lib PoloniusList
+@[default_target] lean_lib Traits