summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Paper.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc/Paper.fst')
-rw-r--r--tests/fstar/misc/Paper.fst11
1 files changed, 5 insertions, 6 deletions
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index ddc5e7a8..c2f47ad1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ())
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -57,15 +57,14 @@ let rec list_nth_mut
begin match l with
| List_Cons x tl ->
if i = 0
- then
- let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
in
- Return (x1, back_'a)
+ Return (x1, back)
| List_Nil -> Fail Failure
end