diff options
| author | Jonathan Protzenko | 2023-02-02 23:49:23 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | f09eabd7c0fce7c20a0124749c841cbf5b550c52 (patch) | |
| tree | bbc761ab3d205981d5da598d5325cc9f4b9d8f4c /tests/lean/hashmap_on_disk/HashmapMain | |
| parent | 40e7df701d246faa453003374206014606ca6b6d (diff) | |
All of the generated code is syntactically correct
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
| -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 |