diff options
| author | Jonathan Protzenko | 2023-01-25 13:12:01 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | e1ee59f6a45482e93901f6a549f594fd6ef15234 (patch) | |
| tree | c9d20fdc675823b058b7d364852c6a5d0bfaf729 /tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | |
| parent | dee74ca1f90acb076289286f6f69df65e63604ce (diff) | |
New directory structure and corresponding extraction, + misc fixes, for Lean
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean new file mode 100644 index 00000000..87b10c59 --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -0,0 +1,13 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: opaque function definitions +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) + |