diff options
| author | Nadrieril | 2024-06-18 12:12:05 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-06-18 12:12:05 +0200 |
| commit | 082661f0d9d1bb1196ef8e1d57b3f2b4922b3d8e (patch) | |
| tree | cb80870b80b3700b003226e62acdf768be143a1c /tests/lean/Arrays.lean | |
| parent | aa5948d7f9fd9b2d0ce18657215dae6877ebd996 (diff) | |
Bump charon
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Arrays.lean | 10 |
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 |