From b11b30564ad550e130e218c2ad29423e5096e66a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 5 Mar 2022 18:46:58 +0100
Subject: Regenerate Paper.fst

---
 tests/misc/Paper.fst | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'tests/misc')

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
+
-- 
cgit v1.2.3