From 3adbe18d36df3767e98f30b760ccd9c6ace640ad Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 17:01:16 +0200
Subject: Rename some subdirectories for consistency

---
 tests/coq/hashmap_main/HashmapMain_FunsExternal.v | 24 +++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/coq/hashmap_main/HashmapMain_FunsExternal.v

(limited to 'tests/coq/hashmap_main/HashmapMain_FunsExternal.v')

diff --git a/tests/coq/hashmap_main/HashmapMain_FunsExternal.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal.v
new file mode 100644
index 00000000..fb5f23cd
--- /dev/null
+++ b/tests/coq/hashmap_main/HashmapMain_FunsExternal.v
@@ -0,0 +1,24 @@
+(** [hashmap_main]: external function declarations *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_FunsExternal.
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_FunsExternal.
-- 
cgit v1.2.3