diff options
Diffstat (limited to 'tests/coq/hashmap_on_disk/HashmapMain_Opaque.v')
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Opaque.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 5e376239..a0e9003d 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -10,12 +10,14 @@ Require Export HashmapMain_Types. Import HashmapMain_Types. Module HashmapMain_Opaque. -(** [hashmap_main::hashmap_utils::deserialize]: forward function *) +(** [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 *) +(** [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) . |