From 7ca25ab5c3e686eaca2716d003bfb04e742209ec Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 15 May 2022 22:35:23 +0200
Subject: Regenerate the F* files

---
 tests/misc/Paper.fst | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'tests/misc/Paper.fst')

diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index d162519a..424889ef 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -59,9 +59,9 @@ type list_t (t : Type0) =
 let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return x
-    | _ ->
+    if i = 0
+    then Return x
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -70,7 +70,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
         | Return x0 -> Return x0
         end
       end
-    end
   | ListNil -> Fail
   end
 
@@ -79,9 +78,9 @@ let rec list_nth_mut_back
   (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return (ListCons ret tl)
-    | _ ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -90,7 +89,6 @@ let rec list_nth_mut_back
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-    end
   | ListNil -> Fail
   end
 
-- 
cgit v1.2.3