From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 tests/lean/Tests.lean | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 tests/lean/Tests.lean

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

diff --git a/tests/lean/Tests.lean b/tests/lean/Tests.lean
deleted file mode 100644
index 9b12270e..00000000
--- a/tests/lean/Tests.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import BetreeMain
-import Constants
-import External
-import Hashmap
-import HashmapMain
-import Loops
-import NoNestedBorrows
-import Paper
-import PoloniusList
-- 
cgit v1.2.3