diff options
Diffstat (limited to 'tests/fstar/misc/Paper.fst')
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 11 |
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 |