summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
blob: ce618a6c79aafe0f8c60a69be87e038e3ecc4310 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [hashmap_main]: opaque function definitions
import Base.Primitives
import HashmapMain.Types

structure OpaqueDefs 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)