diff options
| author | Jonathan Protzenko | 2023-02-02 23:36:14 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | 40e7df701d246faa453003374206014606ca6b6d (patch) | |
| tree | 4f4a199c90ce53937eae8ec4ecb9e0d1f7564a2c /tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | |
| parent | dad646759a3ab9175c8797f144dec9d8e07b54b3 (diff) | |
WIP
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index 87b10c59..8b41934d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -3,11 +3,13 @@ import Base.Primitives import HashmapMain.Types -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils_deserialize_fwd - : state -> result (state × (hashmap_hash_map_t UInt64)) - -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils_serialize_fwd - : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) - +structure OpaqueDecls where + + /- [hashmap_main::hashmap_utils::deserialize] -/ + hashmap_utils_deserialize_fwd + : state -> result (state × (hashmap_hash_map_t UInt64)) + + /- [hashmap_main::hashmap_utils::serialize] -/ + hashmap_utils_serialize_fwd + : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + |