diff options
author | Son Ho | 2024-04-04 16:08:32 +0200 |
---|---|---|
committer | Son Ho | 2024-04-04 16:08:32 +0200 |
commit | 4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f (patch) | |
tree | 89f6a530a6c251d62156d7c84307c4d316d8ceb3 /tests/lean/HashmapMain | |
parent | 7f7387c5519da00133ad557450695e6d6838f93c (diff) |
Rename Result.ret as Result.ok in the backends
Diffstat (limited to 'tests/lean/HashmapMain')
0 files changed, 0 insertions, 0 deletions