From 051e2a19f3268d272a0acd0425d2107ebea020c5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 13:46:55 +0100
Subject: Reorganize the Lean tests and extract the Polonius tests to Lean

---
 tests/lean/misc/constants/lakefile.lean | 18 ------------------
 1 file changed, 18 deletions(-)
 delete mode 100644 tests/lean/misc/constants/lakefile.lean

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

diff --git a/tests/lean/misc/constants/lakefile.lean b/tests/lean/misc/constants/lakefile.lean
deleted file mode 100644
index ed8eebc2..00000000
--- a/tests/lean/misc/constants/lakefile.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Lake
-open Lake DSL
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
-package «constants» {
-  -- add package configuration options here
-}
-
-lean_lib «Base» {
-  -- add library configuration options here
-}
-
-lean_lib «Constants» {
-  -- add library configuration options here
-}
-
-- 
cgit v1.2.3