summaryrefslogtreecommitdiff
path: root/tests/misc/Paper.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/misc/Paper.fst')
-rw-r--r--tests/misc/Paper.fst36
1 files changed, 18 insertions, 18 deletions
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index 1278733b..a6ec184c 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -32,19 +32,19 @@ let choose_back
let test_choose_fwd : result unit =
begin match choose_fwd i32 true 0 0 with
| Fail -> Fail
- | Return i ->
- begin match i32_add i 1 with
+ | Return z ->
+ begin match i32_add z 1 with
| Fail -> Fail
- | Return z ->
- if not (z = 1)
+ | Return z0 ->
+ if not (z0 = 1)
then Fail
else
- begin match choose_back i32 true 0 0 z with
+ begin match choose_back i32 true 0 0 z0 with
| Fail -> Fail
- | Return (i0, i1) ->
- if not (i0 = 1)
+ | Return (i, i0) ->
+ if not (i = 1)
then Fail
- else if not (i1 = 0) then Fail else Return ()
+ else if not (i0 = 0) then Fail else Return ()
end
end
end
@@ -115,16 +115,16 @@ let test_nth_fwd : result unit =
let l1 = ListCons 2 l0 in
begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
| Fail -> Fail
- | Return i ->
- begin match i32_add i 1 with
+ | Return x ->
+ begin match i32_add x 1 with
| Fail -> Fail
- | Return x ->
- begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x with
+ | Return x0 ->
+ begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
| Fail -> Fail
| Return l2 ->
begin match sum_fwd l2 with
| Fail -> Fail
- | Return i0 -> if not (i0 = 7) then Fail else Return ()
+ | Return i -> if not (i = 7) then Fail else Return ()
end
end
end
@@ -138,13 +138,13 @@ let call_choose_fwd (p : (u32 & u32)) : result u32 =
let (px, py) = p in
begin match choose_fwd u32 true px py with
| Fail -> Fail
- | Return i ->
- begin match u32_add i 1 with
+ | Return pz ->
+ begin match u32_add pz 1 with
| Fail -> Fail
- | Return pz ->
- begin match choose_back u32 true px py pz with
+ | Return pz0 ->
+ begin match choose_back u32 true px py pz0 with
| Fail -> Fail
- | Return (i0, _) -> Return i0
+ | Return (i, _) -> Return i
end
end
end