diff options
| author | Son Ho | 2023-07-05 15:09:07 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-05 15:09:07 +0200 |
| commit | c07721dedb2cfe4c726c42606e623395cdfe5b80 (patch) | |
| tree | 5af53eec3c92000aabe2e36b92215ed635aa7a2a /tests/lean/HashmapMain/FunsExternal.lean | |
| parent | 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 (diff) | |
Simplify the generated names for the types in Lean
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/HashmapMain/FunsExternal.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean index d917b485..3689dd45 100644 --- a/tests/lean/HashmapMain/FunsExternal.lean +++ b/tests/lean/HashmapMain/FunsExternal.lean @@ -8,10 +8,10 @@ open hashmap_main /- [hashmap_main::hashmap_utils::deserialize] -/ def hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) := + : State → Result (State × (hashmap.HashMap U64)) := fun _ => .fail .panic /- [hashmap_main::hashmap_utils::serialize] -/ def hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) := + : hashmap.HashMap U64 → State → Result (State × Unit) := fun _ _ => .fail .panic |