summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml')
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml15
1 files changed, 0 insertions, 15 deletions
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
deleted file mode 100644
index f7221d92..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ /dev/null
@@ -1,15 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: external function declarations *)
-open primitivesLib divDefLib
-open hashmapMain_TypesTheory
-
-val _ = new_theory "hashmapMain_Opaque"
-
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
- “:state -> (state # u64 hashmap_hash_map_t) result”)
-
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
- “:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
-
-val _ = export_theory ()