summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/Hashmap/Funs.lean4
-rw-r--r--tests/lean/Hashmap/FunsExternal.lean8
-rw-r--r--tests/lean/Hashmap/FunsExternal_Template.lean9
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)