From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:58:44 +0200
Subject: Regenerate the test files

---
 tests/fstar/misc/Loops.Funs.fst | 83 ++++++++++++++++++++---------------------
 1 file changed, 41 insertions(+), 42 deletions(-)

(limited to 'tests/fstar/misc/Loops.Funs.fst')

diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 7c099da2..93683deb 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a, back_'b)
+        let back'a = fun ret -> Return (List_Cons ret tl0) in
+        let back'b = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back'a, back'b)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
-          in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1, back_'b1)
+        let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back'a1 =
+          fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in
+        let back'b1 =
+          fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in
+        Return (p, back'a1, back'b1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a =
+        let back =
           fun ret ->
             let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
-        Return ((x0, x1), back_'a)
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
+        let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+        let back1 =
           fun ret ->
-            let* (tl01, tl11) = back_'a ret in
+            let* (tl01, tl11) = back ret in
             Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'b)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'b1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
-- 
cgit v1.2.3