3 files changed, 10 insertions, 11 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index e76912cc..d7ac3b05 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -386,9 +386,9 @@ def HashMap.remove
 def insert_on_disk
   (key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
   do
-  let (st1, hm) ← hashmap_utils.deserialize st
+  let (st1, hm) ← utils.deserialize st
   let hm1 ← HashMap.insert U64 hm key value
-  hashmap_utils.serialize hm1 st1
+  utils.serialize hm1 st1
 
 /- [hashmap::test1]:
    Source: 'tests/src/hashmap.rs', lines 350:0-350:10 -/
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
diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean
index 16b4b6af..2af57d10 100644
--- a/tests/lean/Hashmap/FunsExternal_Template.lean
+++ b/tests/lean/Hashmap/FunsExternal_Template.lean
@@ -6,12 +6,11 @@ import Hashmap.Types
 open Primitives
 open hashmap
 
-/- [hashmap::hashmap_utils::deserialize]:
+/- [hashmap::utils::deserialize]:
    Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
-axiom hashmap_utils.deserialize : State → Result (State × (HashMap U64))
+axiom utils.deserialize : State → Result (State × (HashMap U64))
 
-/- [hashmap::hashmap_utils::serialize]:
+/- [hashmap::utils::serialize]:
    Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
-axiom hashmap_utils.serialize
-  : HashMap U64 → State → Result (State × Unit)
+axiom utils.serialize : HashMap U64 → State → Result (State × Unit)