Start using namespaces in the Lean backend

1 files changed, 17 insertions, 0 deletions

diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean
new file mode 100644
index 00000000..d917b485
--- /dev/null
+++ b/tests/lean/HashmapMain/FunsExternal.lean
@@ -0,0 +1,17 @@
+-- [hashmap_main]: templates for the external functions.
+import Base
+import HashmapMain.Types
+open Primitives
+open hashmap_main
+
+-- TODO: fill those bodies
+
+/- [hashmap_main::hashmap_utils::deserialize] -/
+def hashmap_utils.deserialize_fwd
+  : State → Result (State × (hashmap_hash_map_t U64)) :=
+  fun _ => .fail .panic
+
+/- [hashmap_main::hashmap_utils::serialize] -/
+def hashmap_utils.serialize_fwd
+  : hashmap_hash_map_t U64 → State → Result (State × Unit) :=
+  fun _ _ => .fail .panic