diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Paper.lean | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 03b96903..400406f1 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -8,14 +8,14 @@ namespace paper /- [paper::ref_incr]: Source: 'tests/src/paper.rs', lines 7:0-7:28 -/ def ref_incr (x : I32) : Result I32 := - x + 1#i32 + x + 1i32 /- [paper::test_incr]: Source: 'tests/src/paper.rs', lines 11:0-11:18 -/ def test_incr : Result Unit := do - let x ← ref_incr 0#i32 - if x = 1#i32 + let x ← ref_incr 0i32 + if x = 1i32 then Result.ok () else Result.fail .panic @@ -38,14 +38,14 @@ def choose Source: 'tests/src/paper.rs', lines 26:0-26:20 -/ def test_choose : Result Unit := do - let (z, choose_back) ← choose I32 true 0#i32 0#i32 - let z1 ← z + 1#i32 - if z1 = 1#i32 + let (z, choose_back) ← choose I32 true 0i32 0i32 + let z1 ← z + 1i32 + if z1 = 1i32 then do let (x, y) ← choose_back z1 - if x = 1#i32 - then if y = 0#i32 + if x = 1i32 + then if y = 0i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -66,13 +66,13 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -89,19 +89,19 @@ divergent def sum (l : List I32) : Result I32 := | List.Cons x tl => do let i ← sum tl x + i - | List.Nil => Result.ok 0#i32 + | List.Nil => Result.ok 0i32 /- [paper::test_nth]: Source: 'tests/src/paper.rs', lines 71:0-71:17 -/ def test_nth : Result Unit := do - let l := List.Cons 3#i32 List.Nil - let l1 := List.Cons 2#i32 l - let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32 - let x1 ← x + 1#i32 + let l := List.Cons 3i32 List.Nil + let l1 := List.Cons 2i32 l + let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1i32 l1) 2u32 + let x1 ← x + 1i32 let l2 ← list_nth_mut_back x1 let i ← sum l2 - if i = 7#i32 + if i = 7i32 then Result.ok () else Result.fail .panic @@ -114,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 := do let (px, py) := p let (pz, choose_back) ← choose U32 true px py - let pz1 ← pz + 1#u32 + let pz1 ← pz + 1u32 let (px1, _) ← choose_back pz1 Result.ok px1 |