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')

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