diff options
author | Nadrieril | 2024-05-27 14:59:10 +0200 |
---|---|---|
committer | Nadrieril | 2024-05-27 17:22:56 +0200 |
commit | 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 (patch) | |
tree | 687a640232f17269ad33f1a841817491962d4de9 /tests/coq/hashmap/Hashmap_FunsExternal.v | |
parent | 4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff) |
tests: Merge the hashmap test files
Diffstat (limited to '')
-rw-r--r-- | tests/coq/hashmap/Hashmap_FunsExternal.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/tests/coq/hashmap/Hashmap_FunsExternal.v b/tests/coq/hashmap/Hashmap_FunsExternal.v new file mode 100644 index 00000000..bcf12c17 --- /dev/null +++ b/tests/coq/hashmap/Hashmap_FunsExternal.v @@ -0,0 +1,21 @@ +(** [hashmap]: external functions. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Export Hashmap_Types. +Import Hashmap_Types. +Module Hashmap_FunsExternal. + +(** [hashmap::hashmap_utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) +Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)). + +(** [hashmap::hashmap_utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) +Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit) +. + +End Hashmap_FunsExternal. |