summaryrefslogtreecommitdiff
path: root/tests/lean/HashmapMain/FunsExternal.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/HashmapMain/FunsExternal.lean')
-rw-r--r--tests/lean/HashmapMain/FunsExternal.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean
index d917b485..3689dd45 100644
--- a/tests/lean/HashmapMain/FunsExternal.lean
+++ b/tests/lean/HashmapMain/FunsExternal.lean
@@ -8,10 +8,10 @@ open hashmap_main
/- [hashmap_main::hashmap_utils::deserialize] -/
def hashmap_utils.deserialize_fwd
- : State → Result (State × (hashmap_hash_map_t U64)) :=
+ : State → Result (State × (hashmap.HashMap U64)) :=
fun _ => .fail .panic
/- [hashmap_main::hashmap_utils::serialize] -/
def hashmap_utils.serialize_fwd
- : hashmap_hash_map_t U64 → State → Result (State × Unit) :=
+ : hashmap.HashMap U64 → State → Result (State × Unit) :=
fun _ _ => .fail .panic