diff options
Diffstat (limited to 'tests/lean/Hashmap')
-rw-r--r-- | tests/lean/Hashmap/Funs.lean | 4 | ||||
-rw-r--r-- | tests/lean/Hashmap/FunsExternal.lean | 8 | ||||
-rw-r--r-- | tests/lean/Hashmap/FunsExternal_Template.lean | 9 |
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) |