diff options
| author | Son Ho | 2024-02-02 23:17:30 +0100 |
|---|---|---|
| committer | Son Ho | 2024-02-02 23:17:30 +0100 |
| commit | 5cf7d9c0d6b0bc77f2219e7b8b29badce26d51e8 (patch) | |
| tree | c0b07a0b4c3d03787cdece5d6ab6d06311bd17db /tests/lean/lakefile.lean | |
| parent | 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 (diff) | |
Make progress on fixing the tests
Diffstat (limited to 'tests/lean/lakefile.lean')
| -rw-r--r-- | tests/lean/lakefile.lean | 26 |
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 |