summaryrefslogtreecommitdiff
path: root/tests/lean/Loops.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/Loops.lean10
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