diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index ffe3416a..b0c4d683 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -5,7 +5,7 @@ import HashmapMain.Types import HashmapMain.Opaque import HashmapMain.Clauses.Template -section variable (opaque_defs: OpaqueDecls) +section variable (opaque_defs: OpaqueDefs) /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k @@ -654,5 +654,5 @@ def insert_on_disk_fwd def main_fwd : result Unit := result.ret () /- Unit test for [hashmap_main::main] -/ -#assert (main_fwd = ret ()) +#assert (main_fwd = .ret ()) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index 8b41934d..ce618a6c 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -3,7 +3,7 @@ import Base.Primitives import HashmapMain.Types -structure OpaqueDecls where +structure OpaqueDefs where /- [hashmap_main::hashmap_utils::deserialize] -/ hashmap_utils_deserialize_fwd |