diff options
Diffstat (limited to '')
| -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 |