diff options
| author | Guillaume Boisseau | 2024-06-18 13:49:43 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-18 13:49:43 +0200 |
| commit | 370f2668f0a36fb31ed9abb4ba613dad333cf406 (patch) | |
| tree | d1a6549cdd2f8e20366b8a5feaa1550fc10fe783 /tests/lean/Arrays.lean | |
| parent | 43a9fb0fa5a1c03a7cce575a052f0d4201189d1d (diff) | |
| parent | 926eb538cc35cf9a818a6905ff4ce58eeb3db9c4 (diff) | |
Merge pull request #251 from Nadrieril/bump-charon2
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 |