diff options
Diffstat (limited to 'tests/lean/Arrays.lean')
| -rw-r--r-- | tests/lean/Arrays.lean | 41 |
1 files changed, 13 insertions, 28 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index d637ee13..207f31b9 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -28,31 +28,26 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result ((Slice T) × (Slice T → Result (Array T 32#usize))) := - do - let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s - Result.ret (s1, to_slice_mut_back) + Array.to_slice_mut T 32#usize s /- [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 -/ def array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 -/ def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 -/ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := - let i := Slice.len T s - Result.ret i + Result.ret (Slice.len T s) /- [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 -/ @@ -76,9 +71,7 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result (T × (T → Result (Array T 32#usize))) := - do - let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i - Result.ret (t, index_mut_back) + Array.index_mut_usize T 32#usize s i /- [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 -/ @@ -91,9 +84,7 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result (T × (T → Result (Slice T))) := - do - let (t, index_mut_back) ← Slice.index_mut_usize T s i - Result.ret (t, index_mut_back) + Slice.index_mut_usize T s i /- [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 -/ @@ -127,9 +118,7 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := - do - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x - Result.ret (s, to_slice_mut_back) + Array.to_slice_mut U32 32#usize x /- [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 -/ @@ -313,8 +302,8 @@ def update_all : Result Unit := do let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x let s1 ← update_mut_slice s let _ ← to_slice_mut_back s1 Result.ret () @@ -354,9 +343,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit := /- [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 -/ def non_copyable_array : Result Unit := - do - let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) - Result.ret () + take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 -/ @@ -496,11 +483,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) := Source: 'src/arrays.rs', lines 312:0-318:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len - then - do - let i1 ← i + 1#usize - let _ ← iter_mut_slice_loop len i1 - Result.ret () + then do + let i1 ← i + 1#usize + iter_mut_slice_loop len i1 else Result.ret () /- [arrays::iter_mut_slice]: |