diff options
author | Son Ho | 2024-06-12 14:53:12 +0200 |
---|---|---|
committer | Son Ho | 2024-06-12 14:53:12 +0200 |
commit | cd5542fc82edee11181a43e3a342a2567c929e7e (patch) | |
tree | 45cea441e0a493b67bb33d82c083905524c923b0 /tests/lean/Arrays.lean | |
parent | c8272aeea205ca9cb36e22757473ca2a931a4933 (diff) |
Regenerate the tests
Diffstat (limited to 'tests/lean/Arrays.lean')
-rw-r--r-- | tests/lean/Arrays.lean | 225 |
1 files changed, 110 insertions, 115 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 9748919e..70b4a26b 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -14,34 +14,34 @@ inductive AB := /- [arrays::incr]: Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/ def incr (x : U32) : Result U32 := - x + 1#u32 + x + 1u32 /- [arrays::array_to_shared_slice_]: Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/ def array_to_shared_slice_ - (T : Type) (s : Array T 32#usize) : Result (Slice T) := - Array.to_slice T 32#usize s + (T : Type) (s : Array T 32usize) : Result (Slice T) := + Array.to_slice T 32usize s /- [arrays::array_to_mut_slice_]: Source: 'tests/src/arrays.rs', lines 24:0-24:58 -/ def array_to_mut_slice_ - (T : Type) (s : Array T 32#usize) : - Result ((Slice T) × (Slice T → Result (Array T 32#usize))) + (T : Type) (s : Array T 32usize) : + Result ((Slice T) × (Slice T → Result (Array T 32usize))) := - Array.to_slice_mut T 32#usize s + Array.to_slice_mut T 32usize s /- [arrays::array_len]: Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/ -def array_len (T : Type) (s : Array T 32#usize) : Result Usize := +def array_len (T : Type) (s : Array T 32usize) : Result Usize := do - let s1 ← Array.to_slice T 32#usize s + let s1 ← Array.to_slice T 32usize s Result.ok (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/ -def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := +def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize := do - let s1 ← Array.to_slice T 32#usize s + let s1 ← Array.to_slice T 32usize s Result.ok (Slice.len T s1) /- [arrays::shared_slice_len]: @@ -52,26 +52,26 @@ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := /- [arrays::index_array_shared]: Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/ def index_array_shared - (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := - Array.index_usize T 32#usize s i + (T : Type) (s : Array T 32usize) (i : Usize) : Result T := + Array.index_usize T 32usize s i /- [arrays::index_array_u32]: Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/ -def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := - Array.index_usize U32 32#usize s i +def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 := + Array.index_usize U32 32usize s i /- [arrays::index_array_copy]: Source: 'tests/src/arrays.rs', lines 51:0-51:45 -/ -def index_array_copy (x : Array U32 32#usize) : Result U32 := - Array.index_usize U32 32#usize x 0#usize +def index_array_copy (x : Array U32 32usize) : Result U32 := + Array.index_usize U32 32usize x 0usize /- [arrays::index_mut_array]: Source: 'tests/src/arrays.rs', lines 55:0-55:62 -/ def index_mut_array - (T : Type) (s : Array T 32#usize) (i : Usize) : - Result (T × (T → Result (Array T 32#usize))) + (T : Type) (s : Array T 32usize) (i : Usize) : + Result (T × (T → Result (Array T 32usize))) := - Array.index_mut_usize T 32#usize s i + Array.index_mut_usize T 32usize s i /- [arrays::index_slice]: Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/ @@ -109,22 +109,22 @@ def slice_subslice_mut_ /- [arrays::array_to_slice_shared_]: Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/ -def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := - Array.to_slice U32 32#usize x +def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) := + Array.to_slice U32 32usize x /- [arrays::array_to_slice_mut_]: Source: 'tests/src/arrays.rs', lines 79:0-79:59 -/ def array_to_slice_mut_ - (x : Array U32 32#usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) + (x : Array U32 32usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) := - Array.to_slice_mut U32 32#usize x + Array.to_slice_mut U32 32usize x /- [arrays::array_subslice_shared_]: Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/ def array_subslice_shared_ - (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -132,12 +132,12 @@ def array_subslice_shared_ /- [arrays::array_subslice_mut_]: Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/ def array_subslice_mut_ - (x : Array U32 32#usize) (y : Usize) (z : Usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) + (x : Array U32 32usize) (y : Usize) (z : Usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -146,50 +146,50 @@ def array_subslice_mut_ /- [arrays::index_slice_0]: Source: 'tests/src/arrays.rs', lines 91:0-91:38 -/ def index_slice_0 (T : Type) (s : Slice T) : Result T := - Slice.index_usize T s 0#usize + Slice.index_usize T s 0usize /- [arrays::index_array_0]: Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/ -def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := - Array.index_usize T 32#usize s 0#usize +def index_array_0 (T : Type) (s : Array T 32usize) : Result T := + Array.index_usize T 32usize s 0usize /- [arrays::index_index_array]: Source: 'tests/src/arrays.rs', lines 106:0-106:71 -/ def index_index_array - (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : Result U32 := do - let a ← Array.index_usize (Array U32 32#usize) 32#usize s i - Array.index_usize U32 32#usize a j + let a ← Array.index_usize (Array U32 32usize) 32usize s i + Array.index_usize U32 32usize a j /- [arrays::update_update_array]: Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/ def update_update_array - (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : Result Unit := do let (a, index_mut_back) ← - Array.index_mut_usize (Array U32 32#usize) 32#usize s i - let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j - let a1 ← index_mut_back1 0#u32 + Array.index_mut_usize (Array U32 32usize) 32usize s i + let (_, index_mut_back1) ← Array.index_mut_usize U32 32usize a j + let a1 ← index_mut_back1 0u32 let _ ← index_mut_back a1 Result.ok () /- [arrays::array_local_deep_copy]: Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/ -def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := +def array_local_deep_copy (x : Array U32 32usize) : Result Unit := Result.ok () /- [arrays::take_array]: Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/ -def take_array (a : Array U32 2#usize) : Result Unit := +def take_array (a : Array U32 2usize) : Result Unit := Result.ok () /- [arrays::take_array_borrow]: Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/ -def take_array_borrow (a : Array U32 2#usize) : Result Unit := +def take_array_borrow (a : Array U32 2usize) : Result Unit := Result.ok () /- [arrays::take_slice]: @@ -204,70 +204,67 @@ def take_mut_slice (s : Slice U32) : Result (Slice U32) := /- [arrays::const_array]: Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/ -def const_array : Result (Array U32 2#usize) := - Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ]) +def const_array : Result (Array U32 2usize) := + Result.ok (Array.make U32 2usize [ 0u32, 0u32 ]) /- [arrays::const_slice]: Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/ def const_slice : Result Unit := do - let _ ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) Result.ok () /- [arrays::take_all]: Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/ def take_all : Result Unit := do - let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← take_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let _ ← take_slice s let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let s2 ← take_mut_slice s1 let _ ← to_slice_mut_back s2 Result.ok () /- [arrays::index_array]: Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/ -def index_array (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def index_array (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::index_array_borrow]: Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/ -def index_array_borrow (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def index_array_borrow (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::index_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 165:0-165:42 -/ def index_slice_u32_0 (x : Slice U32) : Result U32 := - Slice.index_usize U32 x 0#usize + Slice.index_usize U32 x 0usize /- [arrays::index_mut_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 169:0-169:50 -/ def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← Slice.index_usize U32 x 0#usize + let i ← Slice.index_usize U32 x 0usize Result.ok (i, x) /- [arrays::index_all]: Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/ def index_all : Result U32 := do - let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) let i2 ← i + i1 - let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) let i4 ← i2 + i3 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let i5 ← index_slice_u32_0 s let i6 ← i4 + i5 let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 let i8 ← i6 + i7 let _ ← to_slice_mut_back s2 @@ -275,35 +272,35 @@ def index_all : Result U32 := /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ -def update_array (x : Array U32 2#usize) : Result Unit := +def update_array (x : Array U32 2usize) : Result Unit := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize - let _ ← index_mut_back 1#u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize + let _ ← index_mut_back 1u32 Result.ok () /- [arrays::update_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/ def update_array_mut_borrow - (x : Array U32 2#usize) : Result (Array U32 2#usize) := + (x : Array U32 2usize) : Result (Array U32 2usize) := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize - index_mut_back 1#u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize + index_mut_back 1u32 /- [arrays::update_mut_slice]: Source: 'tests/src/arrays.rs', lines 193:0-193:38 -/ def update_mut_slice (x : Slice U32) : Result (Slice U32) := do - let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize - index_mut_back 1#u32 + let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0usize + index_mut_back 1u32 /- [arrays::update_all]: Source: 'tests/src/arrays.rs', lines 197:0-197:19 -/ 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 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 _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let x ← update_array_mut_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2usize x let s1 ← update_mut_slice s let _ ← to_slice_mut_back s1 Result.ok () @@ -313,37 +310,37 @@ def update_all : Result Unit := def range_all : Result Unit := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) - (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) - { start := 1#usize, end_ := 3#usize } + (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ]) + { start := 1usize, end_ := 3usize } let s1 ← update_mut_slice s let _ ← index_mut_back s1 Result.ok () /- [arrays::deref_array_borrow]: Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/ -def deref_array_borrow (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def deref_array_borrow (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::deref_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 222:0-222:54 -/ def deref_array_mut_borrow - (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) := + (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) := do - let i ← Array.index_usize U32 2#usize x 0#usize + let i ← Array.index_usize U32 2usize x 0usize Result.ok (i, x) /- [arrays::take_array_t]: Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/ -def take_array_t (a : Array AB 2#usize) : Result Unit := +def take_array_t (a : Array AB 2usize) : Result Unit := Result.ok () /- [arrays::non_copyable_array]: Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/ def non_copyable_array : Result Unit := - take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) + take_array_t (Array.make AB 2usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/ @@ -354,14 +351,14 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := do let i2 ← Slice.index_usize U32 s i let sum3 ← sum1 + i2 - let i3 ← i + 1#usize + let i3 ← i + 1usize sum_loop s sum3 i3 else Result.ok sum1 /- [arrays::sum]: Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/ def sum (s : Slice U32) : Result U32 := - sum_loop s 0#u32 0#usize + sum_loop s 0u32 0usize /- [arrays::sum2]: loop 0: Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/ @@ -375,7 +372,7 @@ divergent def sum2_loop let i3 ← Slice.index_usize U32 s2 i let i4 ← i2 + i3 let sum3 ← sum1 + i4 - let i5 ← i + 1#usize + let i5 ← i + 1usize sum2_loop s s2 sum3 i5 else Result.ok sum1 @@ -385,7 +382,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := let i := Slice.len U32 s let i1 := Slice.len U32 s2 if i = i1 - then sum2_loop s s2 0#u32 0#usize + then sum2_loop s s2 0u32 0usize else Result.fail .panic /- [arrays::f0]: @@ -393,9 +390,9 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := def f0 : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize - let s1 ← index_mut_back 1#u32 + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0usize + let s1 ← index_mut_back 1u32 let _ ← to_slice_mut_back s1 Result.ok () @@ -404,9 +401,9 @@ def f0 : Result Unit := def f1 : Result Unit := do let (_, index_mut_back) ← - Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize - let _ ← index_mut_back 1#u32 + Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + 0usize + let _ ← index_mut_back 1u32 Result.ok () /- [arrays::f2]: @@ -416,8 +413,8 @@ def f2 (i : U32) : Result Unit := /- [arrays::f4]: Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/ -def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize +def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -427,34 +424,32 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := def f3 : Result U32 := do let i ← - Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize + Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize let _ ← f2 i - let b := Array.repeat U32 32#usize 0#u32 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let s1 ← f4 b 16#usize 18#usize + let b := Array.repeat U32 32usize 0u32 + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + let s1 ← f4 b 16usize 18usize sum2 s s1 /- [arrays::SZ] Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/ -def SZ_body : Result Usize := Result.ok 32#usize +def SZ_body : Result Usize := Result.ok 32usize def SZ : Usize := eval_global SZ_body /- [arrays::f5]: Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/ -def f5 (x : Array U32 32#usize) : Result U32 := - Array.index_usize U32 32#usize x 0#usize +def f5 (x : Array U32 32usize) : Result U32 := + Array.index_usize U32 32usize x 0usize /- [arrays::ite]: Source: 'tests/src/arrays.rs', lines 297:0-297:12 -/ def ite : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (_, s1) ← index_mut_slice_u32_0 s let (s2, to_slice_mut_back1) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (_, s3) ← index_mut_slice_u32_0 s2 let _ ← to_slice_mut_back1 s3 let _ ← to_slice_mut_back s1 @@ -468,8 +463,8 @@ divergent def zero_slice_loop then do let (_, index_mut_back) ← Slice.index_mut_usize U8 a i - let i1 ← i + 1#usize - let a1 ← index_mut_back 0#u8 + let i1 ← i + 1usize + let a1 ← index_mut_back 0u8 zero_slice_loop a1 i1 len else Result.ok a @@ -477,14 +472,14 @@ divergent def zero_slice_loop Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/ def zero_slice (a : Slice U8) : Result (Slice U8) := let len := Slice.len U8 a - zero_slice_loop a 0#usize len + zero_slice_loop a 0usize len /- [arrays::iter_mut_slice]: loop 0: Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len then do - let i1 ← i + 1#usize + let i1 ← i + 1usize iter_mut_slice_loop len i1 else Result.ok () @@ -493,7 +488,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := def iter_mut_slice (a : Slice U8) : Result (Slice U8) := do let len := Slice.len U8 a - let _ ← iter_mut_slice_loop len 0#usize + let _ ← iter_mut_slice_loop len 0usize Result.ok a /- [arrays::sum_mut_slice]: loop 0: @@ -506,7 +501,7 @@ divergent def sum_mut_slice_loop do let i2 ← Slice.index_usize U32 a i let s1 ← s + i2 - let i3 ← i + 1#usize + let i3 ← i + 1usize sum_mut_slice_loop a i3 s1 else Result.ok s @@ -514,7 +509,7 @@ divergent def sum_mut_slice_loop Source: 'tests/src/arrays.rs', lines 323:0-323:42 -/ def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← sum_mut_slice_loop a 0#usize 0#u32 + let i ← sum_mut_slice_loop a 0usize 0u32 Result.ok (i, a) end arrays |