Add the generated HOL4 files

1 files changed, 15 insertions, 0 deletions

diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
new file mode 100644
index 00000000..5f6bcbb4
--- /dev/null
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: opaque function definitions *)
+open primitivesLib divDefLib
+open hashmapMain_TypesTheory
+
+val _ = new_theory "hashmapMain_Opaque"
+
+
+val _ = new_constant ("hashmap_utils_deserialize_fwd",
+  “:state -> (state # u64 hashmap_hash_map_t) result”)
+
+val _ = new_constant ("hashmap_utils_serialize_fwd",
+  “:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
+
+val _ = export_theory ()