summaryrefslogtreecommitdiff
path: root/tests/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/misc')
-rw-r--r--tests/misc/Paper.fst16
1 files changed, 16 insertions, 0 deletions
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index be4326d7..1278733b 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -133,3 +133,19 @@ let test_nth_fwd : result unit =
(** Unit test for [paper::test_nth] *)
let _ = assert_norm (test_nth_fwd = Return ())
+(** [paper::call_choose] *)
+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
+ | Fail -> Fail
+ | Return pz ->
+ begin match choose_back u32 true px py pz with
+ | Fail -> Fail
+ | Return (i0, _) -> Return i0
+ end
+ end
+ end
+