From 5cf7d9c0d6b0bc77f2219e7b8b29badce26d51e8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:17:30 +0100
Subject: Make progress on fixing the tests

---
 tests/lean/lakefile.lean | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'tests/lean/lakefile.lean')

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
-- 
cgit v1.2.3


From 7ecf28dc36f724a4ab4b3b4976421e4e4c397f3b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:33:20 +0100
Subject: Rename and regenerate some files

---
 tests/lean/lakefile.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/lakefile.lean')

diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index 502d8098..781fc8b8 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -6,9 +6,8 @@ require mathlib from git
 
 require base from "../../backends/lean"
 
-package «Tests» {}
+package «tests» {}
 
-@[default_target] lean_lib array
 @[default_target] lean_lib Tutorial
 @[default_target] lean_lib BetreeMain
 @[default_target] lean_lib Constants
@@ -19,4 +18,5 @@ package «Tests» {}
 @[default_target] lean_lib NoNestedBorrows
 @[default_target] lean_lib Paper
 @[default_target] lean_lib PoloniusList
+@[default_target] lean_lib Arrays
 @[default_target] lean_lib Traits
-- 
cgit v1.2.3