diff options
| -rw-r--r-- | tests/misc/Paper.fst | 16 |
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 + |