summaryrefslogtreecommitdiff
path: root/tests/lean/HashmapMain/Opaque.lean
blob: a410b253ee4b873d7d31a40366b93ab928dc817d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- [hashmap_main]: opaque function definitions
import Base
import HashmapMain.Types
open Primitives

namespace hashmap_main

structure OpaqueDefs where
  
  /- [hashmap_main::hashmap_utils::deserialize] -/
  hashmap_utils.deserialize_fwd
    : State  Result (State × (hashmap_hash_map_t U64))
  
  /- [hashmap_main::hashmap_utils::serialize] -/
  hashmap_utils.serialize_fwd
    : hashmap_hash_map_t U64  State  Result (State × Unit)
  
end hashmap_main