diff options
author | Son Ho | 2024-04-04 11:58:44 +0200 |
---|---|---|
committer | Son Ho | 2024-04-04 11:58:44 +0200 |
commit | 975ddb208f18cb4ba46293dd788c46eb1ce43938 (patch) | |
tree | fe3c083f8c180f71bdc1ac8f22c1aaff51c30671 /tests/fstar/misc/Loops.Funs.fst | |
parent | 795e2107e305d425efdf6071b29f186cae83656b (diff) |
Regenerate the test files
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 83 |
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 |