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/HashmapMain/ExternalFuns.lean | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 tests/lean/HashmapMain/ExternalFuns.lean

(limited to 'tests/lean/HashmapMain/ExternalFuns.lean')

diff --git a/tests/lean/HashmapMain/ExternalFuns.lean b/tests/lean/HashmapMain/ExternalFuns.lean
deleted file mode 100644
index bc831158..00000000
--- a/tests/lean/HashmapMain/ExternalFuns.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Base
-import HashmapMain.Types
-import HashmapMain.Opaque
-
-namespace HashmapMain
-
-def opaque_defs : OpaqueDefs := by sorry
-
-end HashmapMain
-- 
cgit v1.2.3