Merge pull request #31 from AeneasVerif/son_lean_backend

Improve 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..b394b32b
--- /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
+  : State → Result (State × (hashmap.HashMap U64)) :=
+  fun _ => .fail .panic
+
+/- [hashmap_main::hashmap_utils::serialize] -/
+def hashmap_utils.serialize
+  : hashmap.HashMap U64 → State → Result (State × Unit) :=
+  fun _ _ => .fail .panic