summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap/FunsExternal.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Hashmap/FunsExternal.lean')
-rw-r--r--tests/lean/Hashmap/FunsExternal.lean8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/lean/Hashmap/FunsExternal.lean b/tests/lean/Hashmap/FunsExternal.lean
index 7454696b..329e5d82 100644
--- a/tests/lean/Hashmap/FunsExternal.lean
+++ b/tests/lean/Hashmap/FunsExternal.lean
@@ -6,14 +6,14 @@ open hashmap
-- TODO: fill those bodies
-/- [hashmap::hashmap_utils::deserialize]:
+/- [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
-def hashmap_utils.deserialize
+def utils.deserialize
: State → Result (State × (HashMap U64)) :=
fun _ => .fail .panic
-/- [hashmap::hashmap_utils::serialize]:
+/- [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
-def hashmap_utils.serialize
+def utils.serialize
: HashMap U64 → State → Result (State × Unit) :=
fun _ _ => .fail .panic