summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean
blob: 164995f037f89d5a41186335ecef2fd5f145dfa8 (plain)
1
2
3
4
5
6
7
8
9
10
11
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [hashmap_main]: opaque function definitions
import Hashmap.Primitives
import Hashmap.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)