diff options
| author | Nadrieril | 2024-05-28 11:18:35 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-05-28 11:36:31 +0200 |
| commit | c4d2af051c18c4c81b1e57a45210c37c89c8330f (patch) | |
| tree | a72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests/lean/Hashmap | |
| parent | c81c96f20b1dbf428a9ed42e83b910e798e1a225 (diff) | |
tests: Rename hashmap_utils -> utils
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) |