From 082661f0d9d1bb1196ef8e1d57b3f2b4922b3d8e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Jun 2024 12:12:05 +0200
Subject: Bump charon

---
 tests/lean/Loops.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/lean/Loops.lean')

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
-- 
cgit v1.2.3