diff options
author | Son HO | 2024-04-11 20:32:15 +0200 |
---|---|---|
committer | GitHub | 2024-04-11 20:32:15 +0200 |
commit | 77d74452489f85f558efe07d72d0200c80b16444 (patch) | |
tree | 810c6504b8e5b2fcde58841e25079d5e8c8e92ae /tests/lean/Demo/Demo.lean | |
parent | 4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (diff) | |
parent | 2f8aa9b47acb5c98aed91c29b04f71099452e781 (diff) |
Merge pull request #123 from AeneasVerif/son/clean
Cleanup the code in preparation of the nested loops
Diffstat (limited to '')
-rw-r--r-- | tests/lean/Demo/Demo.lean | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 6d9fef8e..3a3aeb96 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -12,10 +12,10 @@ def choose Result (T × (T → Result (T × T))) := if b - then let back := fun ret => Result.ret (ret, y) - Result.ret (x, back) - else let back := fun ret => Result.ret (x, ret) - Result.ret (y, back) + then let back := fun ret => Result.ok (ret, y) + Result.ok (x, back) + else let back := fun ret => Result.ok (x, ret) + Result.ok (y, back) /- [demo::mul2_add1]: Source: 'src/demo.rs', lines 13:0-13:31 -/ @@ -43,7 +43,7 @@ def use_incr : Result Unit := let x ← incr 0#u32 let x1 ← incr x let _ ← incr x1 - Result.ret () + Result.ok () /- [demo::CList] Source: 'src/demo.rs', lines 34:0-34:17 -/ @@ -57,7 +57,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => if i = 0#u32 - then Result.ret x + then Result.ok x else do let i1 ← i - 1#u32 list_nth T tl i1 @@ -73,8 +73,8 @@ divergent def list_nth_mut | CList.CCons x tl => if i = 0#u32 then - let back := fun ret => Result.ret (CList.CCons ret tl) - Result.ret (x, back) + let back := fun ret => Result.ok (CList.CCons ret tl) + Result.ok (x, back) else do let i1 ← i - 1#u32 @@ -83,8 +83,8 @@ divergent def list_nth_mut fun ret => do let tl1 ← list_nth_mut_back ret - Result.ret (CList.CCons x tl1) - Result.ret (t, back) + Result.ok (CList.CCons x tl1) + Result.ok (t, back) | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: loop 0: @@ -97,8 +97,8 @@ divergent def list_nth_mut1_loop | CList.CCons x tl => if i = 0#u32 then - let back := fun ret => Result.ret (CList.CCons ret tl) - Result.ret (x, back) + let back := fun ret => Result.ok (CList.CCons ret tl) + Result.ok (x, back) else do let i1 ← i - 1#u32 @@ -106,8 +106,8 @@ divergent def list_nth_mut1_loop let back1 := fun ret => do let tl1 ← back ret - Result.ret (CList.CCons x tl1) - Result.ret (t, back1) + Result.ok (CList.CCons x tl1) + Result.ok (t, back1) | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: @@ -122,7 +122,7 @@ def list_nth_mut1 Source: 'src/demo.rs', lines 80:0-80:28 -/ divergent def i32_id (i : I32) : Result I32 := if i = 0#i32 - then Result.ret 0#i32 + then Result.ok 0#i32 else do let i1 ← i - 1#i32 let i2 ← i32_id i1 @@ -142,9 +142,9 @@ divergent def list_tail fun ret => do let tl1 ← list_tail_back ret - Result.ret (CList.CCons t tl1) - Result.ret (c, back) - | CList.CNil => Result.ret (CList.CNil, Result.ret) + Result.ok (CList.CCons t tl1) + Result.ok (c, back) + | CList.CNil => Result.ok (CList.CNil, Result.ok) /- Trait declaration: [demo::Counter] Source: 'src/demo.rs', lines 97:0-97:17 -/ @@ -156,7 +156,7 @@ structure Counter (Self : Type) where def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do let self1 ← self + 1#usize - Result.ret (self, self1) + Result.ok (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] Source: 'src/demo.rs', lines 101:0-101:22 -/ |