summaryrefslogtreecommitdiff
path: root/tests/lean/Arrays.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Arrays.lean')
-rw-r--r--tests/lean/Arrays.lean10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index bb97d5c4..bdaa7380 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -349,7 +349,7 @@ def non_copyable_array : Result Unit :=
take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
/- [arrays::sum]: loop 0:
- Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
+ Source: 'tests/src/arrays.rs', lines 247:4-253:1 -/
divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
let i1 := Slice.len U32 s
if i < i1
@@ -367,7 +367,7 @@ def sum (s : Slice U32) : Result U32 :=
sum_loop s 0#u32 0#usize
/- [arrays::sum2]: loop 0:
- Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
+ Source: 'tests/src/arrays.rs', lines 258:4-264:1 -/
divergent def sum2_loop
(s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
let i1 := Slice.len U32 s
@@ -464,7 +464,7 @@ def ite : Result Unit :=
Result.ok ()
/- [arrays::zero_slice]: loop 0:
- Source: 'tests/src/arrays.rs', lines 306:0-313:1 -/
+ Source: 'tests/src/arrays.rs', lines 308:4-313:1 -/
divergent def zero_slice_loop
(a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
if i < len
@@ -483,7 +483,7 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
zero_slice_loop a 0#usize len
/- [arrays::iter_mut_slice]: loop 0:
- Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/
+ Source: 'tests/src/arrays.rs', lines 317:4-321:1 -/
divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
if i < len
then do
@@ -500,7 +500,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
Result.ok a
/- [arrays::sum_mut_slice]: loop 0:
- Source: 'tests/src/arrays.rs', lines 323:0-331:1 -/
+ Source: 'tests/src/arrays.rs', lines 325:4-331:1 -/
divergent def sum_mut_slice_loop
(a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
let i1 := Slice.len U32 a