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/Loops.lean | |
parent | aa5948d7f9fd9b2d0ce18657215dae6877ebd996 (diff) |
Bump charon
Diffstat (limited to 'tests/lean/Loops.lean')
-rw-r--r-- | tests/lean/Loops.lean | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index e676336e..6435cabb 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -9,7 +9,7 @@ set_option linter.unusedVariables false namespace loops /- [loops::sum]: loop 0: - Source: 'tests/src/loops.rs', lines 8:0-18:1 -/ + Source: 'tests/src/loops.rs', lines 10:4-18:1 -/ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max then do @@ -24,7 +24,7 @@ def sum (max : U32) : Result U32 := sum_loop max 0#u32 0#u32 /- [loops::sum_with_mut_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 23:0-35:1 -/ + Source: 'tests/src/loops.rs', lines 25:4-35:1 -/ divergent def sum_with_mut_borrows_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max @@ -41,7 +41,7 @@ def sum_with_mut_borrows (max : U32) : Result U32 := sum_with_mut_borrows_loop max 0#u32 0#u32 /- [loops::sum_with_shared_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 38:0-52:1 -/ + Source: 'tests/src/loops.rs', lines 40:4-52:1 -/ divergent def sum_with_shared_borrows_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max @@ -58,7 +58,7 @@ def sum_with_shared_borrows (max : U32) : Result U32 := sum_with_shared_borrows_loop max 0#u32 0#u32 /- [loops::sum_array]: loop 0: - Source: 'tests/src/loops.rs', lines 54:0-62:1 -/ + Source: 'tests/src/loops.rs', lines 56:4-62:1 -/ divergent def sum_array_loop (N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 := if i < N @@ -76,7 +76,7 @@ def sum_array (N : Usize) (a : Array U32 N) : Result U32 := sum_array_loop N a 0#usize 0#u32 /- [loops::clear]: loop 0: - Source: 'tests/src/loops.rs', lines 66:0-72:1 -/ + Source: 'tests/src/loops.rs', lines 67:4-72:1 -/ divergent def clear_loop (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := let i1 := alloc.vec.Vec.len U32 v |