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

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

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

diff --git a/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v
new file mode 100644
index 00000000..66835e8c
--- /dev/null
+++ b/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v
@@ -0,0 +1,26 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
+Module HashmapMain_FunsExternal_Template.
+
+(** [hashmap_main::hashmap_utils::deserialize]:
+    Source: 'tests/src/hashmap_utils.rs', lines 11:0-11:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]:
+    Source: 'tests/src/hashmap_utils.rs', lines 6:0-6:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_FunsExternal_Template.
-- 
cgit v1.2.3