summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Loops.Funs.fst
diff options
context:
space:
mode:
authorSon Ho2024-04-04 11:58:44 +0200
committerSon Ho2024-04-04 11:58:44 +0200
commit975ddb208f18cb4ba46293dd788c46eb1ce43938 (patch)
treefe3c083f8c180f71bdc1ac8f22c1aaff51c30671 /tests/fstar/misc/Loops.Funs.fst
parent795e2107e305d425efdf6071b29f186cae83656b (diff)
Regenerate the test files
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/Loops.Funs.fst83
1 files changed, 41 insertions, 42 deletions
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