From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

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

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

diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 3f075347..0f3d77c2 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -23,14 +23,14 @@ def sum (max : U32) : Result U32 :=
 /- [loops::sum_with_mut_borrows]: loop 0:
    Source: 'src/loops.rs', lines 19:0-31:1 -/
 divergent def sum_with_mut_borrows_loop
-  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
-  if mi < max
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
   then
     do
-    let ms1 ← ms + mi
-    let mi1 ← mi + 1#u32
-    sum_with_mut_borrows_loop max mi1 ms1
-  else ms * 2#u32
+    let ms ← s + i
+    let mi ← i + 1#u32
+    sum_with_mut_borrows_loop max mi ms
+  else s * 2#u32
 
 /- [loops::sum_with_mut_borrows]:
    Source: 'src/loops.rs', lines 19:0-19:44 -/
@@ -187,13 +187,13 @@ def get_elem_mut
   Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
   :=
   do
-  let (l, index_mut_back) ←
+  let (ls, index_mut_back) ←
     alloc.vec.Vec.index_mut (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  let (i, back) ← get_elem_mut_loop x l
+  let (i, back) ← get_elem_mut_loop x ls
   let back1 := fun ret => do
-                          let l1 ← back ret
-                          index_mut_back l1
+                          let l ← back ret
+                          index_mut_back l
   Result.ret (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
@@ -211,10 +211,10 @@ divergent def get_elem_shared_loop
 def get_elem_shared
   (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-  let l ←
+  let ls ←
     alloc.vec.Vec.index (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  get_elem_shared_loop x l
+  get_elem_shared_loop x ls
 
 /- [loops::id_mut]:
    Source: 'src/loops.rs', lines 145:0-145:50 -/
-- 
cgit v1.2.3