diff options
Diffstat (limited to 'tests/lean/External')
| -rw-r--r-- | tests/lean/External/Funs.lean | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index cfb2cb3c..78e0f95c 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -26,10 +26,10 @@ def test_new_non_zero_u32 def test_vec : Result Unit := do let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32 - Result.ret () + Result.ok () /- Unit test for [external::test_vec] -/ -#assert (test_vec == Result.ret ()) +#assert (test_vec == Result.ok ()) /- [external::custom_swap]: Source: 'src/external.rs', lines 24:0-24:66 -/ @@ -39,8 +39,8 @@ def custom_swap := do let (st1, (x1, y1)) ← core.mem.swap T x y st - let back := fun ret st2 => Result.ret (st2, (ret, y1)) - Result.ret (st1, (x1, back)) + let back := fun ret st2 => Result.ok (st2, (ret, y1)) + Result.ok (st1, (x1, back)) /- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ @@ -49,7 +49,7 @@ def test_custom_swap do let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st let (_, (x1, y1)) ← custom_swap_back 1#u32 st1 - Result.ret (st1, (x1, y1)) + Result.ok (st1, (x1, y1)) /- [external::test_swap_non_zero]: Source: 'src/external.rs', lines 35:0-35:44 -/ @@ -59,6 +59,6 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) := let (x1, _) := p if x1 = 0#u32 then Result.fail .panic - else Result.ret (st1, x1) + else Result.ok (st1, x1) end external |