From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jul 2023 14:52:23 +0200 Subject: Start using namespaces in the Lean backend --- tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml') diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml index 5f6bcbb4..c38eca01 100644 --- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml +++ b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: opaque function definitions *) +(** [hashmap_main]: external function declarations *) open primitivesLib divDefLib open hashmapMain_TypesTheory -- cgit v1.2.3 From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jul 2023 12:20:28 +0200 Subject: Improve the generated comments --- tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml') diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml index c38eca01..f7221d92 100644 --- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml +++ b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml @@ -6,10 +6,10 @@ open hashmapMain_TypesTheory val _ = new_theory "hashmapMain_Opaque" -val _ = new_constant ("hashmap_utils_deserialize_fwd", +(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd", “:state -> (state # u64 hashmap_hash_map_t) result”) -val _ = new_constant ("hashmap_utils_serialize_fwd", +(** [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 () -- cgit v1.2.3