Regenerate the F* files

10 files changed, 130 insertions, 194 deletions

diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index b11ca399..9b960ce5 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -135,9 +135,9 @@ let rec betree_list_split_at_fwd
   Tot (result ((betree_list_t t) & (betree_list_t t)))
   (decreases (betree_list_split_at_decreases t self n))
   =
-  begin match n with
-  | 0 -> Return (BetreeListNil, self)
-  | _ ->
+  if n = 0
+  then Return (BetreeListNil, self)
+  else
     begin match self with
     | BetreeListCons hd tl ->
       begin match u64_sub n 1 with
@@ -152,7 +152,6 @@ let rec betree_list_split_at_fwd
       end
     | BetreeListNil -> Fail
     end
-  end
 
 (** [betree_main::betree::List::{1}::push_front] *)
 let betree_list_push_front_fwd_back
@@ -528,10 +527,7 @@ and betree_node_lookup_fwd
           let (k, msg) = p in
           if k <> key
           then
-            begin match
-              betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
-                node.betree_internal_id node.betree_internal_pivot
-                node.betree_internal_left node.betree_internal_right) key st0
+            begin match betree_internal_lookup_in_children_fwd node key st0
               with
             | Fail -> Fail
             | Return (st1, opt) ->
@@ -559,10 +555,7 @@ and betree_node_lookup_fwd
               | Return _ -> Return (st0, None)
               end
             | BetreeMessageUpsert ufs ->
-              begin match
-                betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right) key st0
+              begin match betree_internal_lookup_in_children_fwd node key st0
                 with
               | Fail -> Fail
               | Return (st1, v) ->
@@ -572,10 +565,7 @@ and betree_node_lookup_fwd
                 | Fail -> Fail
                 | Return (st2, v0) ->
                   begin match
-                    betree_internal_lookup_in_children_back
-                      (Mkbetree_internal_t node.betree_internal_id
-                      node.betree_internal_pivot node.betree_internal_left
-                      node.betree_internal_right) key st0 with
+                    betree_internal_lookup_in_children_back node key st0 with
                   | Fail -> Fail
                   | Return node0 ->
                     begin match
@@ -601,11 +591,7 @@ and betree_node_lookup_fwd
               end
             end
         | BetreeListNil ->
-          begin match
-            betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
-              node.betree_internal_id node.betree_internal_pivot
-              node.betree_internal_left node.betree_internal_right) key st0
-            with
+          begin match betree_internal_lookup_in_children_fwd node key st0 with
           | Fail -> Fail
           | Return (st1, opt) ->
             begin match
@@ -653,10 +639,7 @@ and betree_node_lookup_back
                 (BetreeListCons (k, msg) l) with
             | Fail -> Fail
             | Return _ ->
-              begin match
-                betree_internal_lookup_in_children_back (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right) key st0
+              begin match betree_internal_lookup_in_children_back node key st0
                 with
               | Fail -> Fail
               | Return node0 -> Return (BetreeNodeInternal node0)
@@ -669,26 +652,17 @@ and betree_node_lookup_back
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageInsert v) l) with
               | Fail -> Fail
-              | Return _ ->
-                Return (BetreeNodeInternal (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right))
+              | Return _ -> Return (BetreeNodeInternal node)
               end
             | BetreeMessageDelete ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageDelete) l) with
               | Fail -> Fail
-              | Return _ ->
-                Return (BetreeNodeInternal (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right))
+              | Return _ -> Return (BetreeNodeInternal node)
               end
             | BetreeMessageUpsert ufs ->
-              begin match
-                betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right) key st0
+              begin match betree_internal_lookup_in_children_fwd node key st0
                 with
               | Fail -> Fail
               | Return (st1, v) ->
@@ -698,10 +672,7 @@ and betree_node_lookup_back
                 | Fail -> Fail
                 | Return (st2, _) ->
                   begin match
-                    betree_internal_lookup_in_children_back
-                      (Mkbetree_internal_t node.betree_internal_id
-                      node.betree_internal_pivot node.betree_internal_left
-                      node.betree_internal_right) key st0 with
+                    betree_internal_lookup_in_children_back node key st0 with
                   | Fail -> Fail
                   | Return node0 ->
                     begin match
@@ -718,12 +689,7 @@ and betree_node_lookup_back
                           betree_store_internal_node_fwd
                             node0.betree_internal_id msgs0 st2 with
                         | Fail -> Fail
-                        | Return (_, _) ->
-                          Return (BetreeNodeInternal (Mkbetree_internal_t
-                            node0.betree_internal_id
-                            node0.betree_internal_pivot
-                            node0.betree_internal_left
-                            node0.betree_internal_right))
+                        | Return (_, _) -> Return (BetreeNodeInternal node0)
                         end
                       end
                     end
@@ -737,10 +703,7 @@ and betree_node_lookup_back
               BetreeListNil with
           | Fail -> Fail
           | Return _ ->
-            begin match
-              betree_internal_lookup_in_children_back (Mkbetree_internal_t
-                node.betree_internal_id node.betree_internal_pivot
-                node.betree_internal_left node.betree_internal_right) key st0
+            begin match betree_internal_lookup_in_children_back node key st0
               with
             | Fail -> Fail
             | Return node0 -> Return (BetreeNodeInternal node0)
@@ -755,9 +718,7 @@ and betree_node_lookup_back
     | Return (_, bindings) ->
       begin match betree_node_lookup_in_bindings_fwd key bindings with
       | Fail -> Fail
-      | Return _ ->
-        Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
-          node.betree_leaf_size))
+      | Return _ -> Return (BetreeNodeLeaf node)
       end
     end
   end
@@ -1323,17 +1284,13 @@ and betree_node_apply_messages_fwd
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
-              betree_internal_flush_fwd (Mkbetree_internal_t
-                node.betree_internal_id node.betree_internal_pivot
-                node.betree_internal_left node.betree_internal_right) params
-                node_id_cnt content0 st0 with
+              betree_internal_flush_fwd node params node_id_cnt content0 st0
+              with
             | Fail -> Fail
             | Return (st1, content1) ->
               begin match
-                betree_internal_flush_back (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right) params
-                  node_id_cnt content0 st0 with
+                betree_internal_flush_back node params node_id_cnt content0 st0
+                with
               | Fail -> Fail
               | Return (node0, _) ->
                 begin match
@@ -1370,8 +1327,7 @@ and betree_node_apply_messages_fwd
             if len >= i
             then
               begin match
-                betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
-                  node.betree_leaf_size) content0 params node_id_cnt st0 with
+                betree_leaf_split_fwd node content0 params node_id_cnt st0 with
               | Fail -> Fail
               | Return (st1, _) ->
                 begin match
@@ -1418,17 +1374,13 @@ and betree_node_apply_messages_back
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
-              betree_internal_flush_fwd (Mkbetree_internal_t
-                node.betree_internal_id node.betree_internal_pivot
-                node.betree_internal_left node.betree_internal_right) params
-                node_id_cnt content0 st0 with
+              betree_internal_flush_fwd node params node_id_cnt content0 st0
+              with
             | Fail -> Fail
             | Return (st1, content1) ->
               begin match
-                betree_internal_flush_back (Mkbetree_internal_t
-                  node.betree_internal_id node.betree_internal_pivot
-                  node.betree_internal_left node.betree_internal_right) params
-                  node_id_cnt content0 st0 with
+                betree_internal_flush_back node params node_id_cnt content0 st0
+                with
               | Fail -> Fail
               | Return (node0, node_id_cnt0) ->
                 begin match
@@ -1436,10 +1388,7 @@ and betree_node_apply_messages_back
                     content1 st1 with
                 | Fail -> Fail
                 | Return (_, _) ->
-                  Return (BetreeNodeInternal (Mkbetree_internal_t
-                    node0.betree_internal_id node0.betree_internal_pivot
-                    node0.betree_internal_left node0.betree_internal_right),
-                    node_id_cnt0)
+                  Return (BetreeNodeInternal node0, node_id_cnt0)
                 end
               end
             end
@@ -1448,11 +1397,7 @@ and betree_node_apply_messages_back
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st0 with
             | Fail -> Fail
-            | Return (_, _) ->
-              Return (BetreeNodeInternal (Mkbetree_internal_t
-                node.betree_internal_id node.betree_internal_pivot
-                node.betree_internal_left node.betree_internal_right),
-                node_id_cnt)
+            | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
             end
         end
       end
@@ -1473,8 +1418,7 @@ and betree_node_apply_messages_back
             if len >= i
             then
               begin match
-                betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
-                  node.betree_leaf_size) content0 params node_id_cnt st0 with
+                betree_leaf_split_fwd node content0 params node_id_cnt st0 with
               | Fail -> Fail
               | Return (st1, new_node) ->
                 begin match
@@ -1483,8 +1427,7 @@ and betree_node_apply_messages_back
                 | Fail -> Fail
                 | Return (_, _) ->
                   begin match
-                    betree_leaf_split_back (Mkbetree_leaf_t node.betree_leaf_id
-                      node.betree_leaf_size) content0 params node_id_cnt st0
+                    betree_leaf_split_back node content0 params node_id_cnt st0
                     with
                   | Fail -> Fail
                   | Return node_id_cnt0 ->
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
 /// The scalar types
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index a97c52b9..83c245fb 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -16,9 +16,9 @@ let rec hash_map_allocate_slots_fwd
   Tot (result (vec (list_t t)))
   (decreases (hash_map_allocate_slots_decreases t slots n))
   =
-  begin match n with
-  | 0 -> Return slots
-  | _ ->
+  if n = 0
+  then Return slots
+  else
     begin match vec_push_back (list_t t) slots ListNil with
     | Fail -> Fail
     | Return slots0 ->
@@ -31,7 +31,6 @@ let rec hash_map_allocate_slots_fwd
         end
       end
     end
-  end
 
 (** [hashmap::HashMap::{0}::new_with_capacity] *)
 let hash_map_new_with_capacity_fwd
@@ -245,35 +244,39 @@ let rec hash_map_move_elements_fwd_back
 (** [hashmap::HashMap::{0}::try_resize] *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  let capacity = vec_len (list_t t) self.hash_map_slots in
-  begin match usize_div 4294967295 2 with
+  begin match scalar_cast U32 Usize 4294967295 with
   | Fail -> Fail
-  | Return n1 ->
-    let (i, i0) = self.hash_map_max_load_factor in
-    begin match usize_div n1 i with
+  | Return max_usize ->
+    let capacity = vec_len (list_t t) self.hash_map_slots in
+    begin match usize_div max_usize 2 with
     | Fail -> Fail
-    | Return i1 ->
-      if capacity <= i1
-      then
-        begin match usize_mul capacity 2 with
-        | Fail -> Fail
-        | Return i2 ->
-          begin match hash_map_new_with_capacity_fwd t i2 i i0 with
+    | Return n1 ->
+      let (i, i0) = self.hash_map_max_load_factor in
+      begin match usize_div n1 i with
+      | Fail -> Fail
+      | Return i1 ->
+        if capacity <= i1
+        then
+          begin match usize_mul capacity 2 with
           | Fail -> Fail
-          | Return ntable ->
-            begin match
-              hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
-              with
+          | Return i2 ->
+            begin match hash_map_new_with_capacity_fwd t i2 i i0 with
             | Fail -> Fail
-            | Return (ntable0, _) ->
-              Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
-                ntable0.hash_map_max_load ntable0.hash_map_slots)
+            | Return ntable ->
+              begin match
+                hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
+                with
+              | Fail -> Fail
+              | Return (ntable0, _) ->
+                Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+                  ntable0.hash_map_max_load ntable0.hash_map_slots)
+              end
             end
           end
-        end
-      else
-        Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
-          self.hash_map_max_load self.hash_map_slots)
+        else
+          Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+            self.hash_map_max_load self.hash_map_slots)
+      end
     end
   end
 
@@ -290,17 +293,11 @@ let hash_map_insert_fwd_back
     | Return i ->
       if i > self0.hash_map_max_load
       then
-        begin match
-          hash_map_try_resize_fwd_back t (Mkhash_map_t
-            self0.hash_map_num_entries self0.hash_map_max_load_factor
-            self0.hash_map_max_load self0.hash_map_slots) with
+        begin match hash_map_try_resize_fwd_back t self0 with
         | Fail -> Fail
         | Return self1 -> Return self1
         end
-      else
-        Return (Mkhash_map_t self0.hash_map_num_entries
-          self0.hash_map_max_load_factor self0.hash_map_max_load
-          self0.hash_map_slots)
+      else Return self0
     end
   end
 
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
 /// The scalar types
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 160df880..d01046ec 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -17,9 +17,9 @@ let rec hashmap_hash_map_allocate_slots_fwd
   Tot (result (vec (hashmap_list_t t)))
   (decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
   =
-  begin match n with
-  | 0 -> Return slots
-  | _ ->
+  if n = 0
+  then Return slots
+  else
     begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
     | Fail -> Fail
     | Return slots0 ->
@@ -32,7 +32,6 @@ let rec hashmap_hash_map_allocate_slots_fwd
         end
       end
     end
-  end
 
 (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
 let hashmap_hash_map_new_with_capacity_fwd
@@ -258,36 +257,40 @@ let rec hashmap_hash_map_move_elements_fwd_back
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
-  let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-  begin match usize_div 4294967295 2 with
+  begin match scalar_cast U32 Usize 4294967295 with
   | Fail -> Fail
-  | Return n1 ->
-    let (i, i0) = self.hashmap_hash_map_max_load_factor in
-    begin match usize_div n1 i with
+  | Return max_usize ->
+    let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_div max_usize 2 with
     | Fail -> Fail
-    | Return i1 ->
-      if capacity <= i1
-      then
-        begin match usize_mul capacity 2 with
-        | Fail -> Fail
-        | Return i2 ->
-          begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
+    | Return n1 ->
+      let (i, i0) = self.hashmap_hash_map_max_load_factor in
+      begin match usize_div n1 i with
+      | Fail -> Fail
+      | Return i1 ->
+        if capacity <= i1
+        then
+          begin match usize_mul capacity 2 with
           | Fail -> Fail
-          | Return ntable ->
-            begin match
-              hashmap_hash_map_move_elements_fwd_back t ntable
-                self.hashmap_hash_map_slots 0 with
+          | Return i2 ->
+            begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
             | Fail -> Fail
-            | Return (ntable0, _) ->
-              Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
-                (i, i0) ntable0.hashmap_hash_map_max_load
-                ntable0.hashmap_hash_map_slots)
+            | Return ntable ->
+              begin match
+                hashmap_hash_map_move_elements_fwd_back t ntable
+                  self.hashmap_hash_map_slots 0 with
+              | Fail -> Fail
+              | Return (ntable0, _) ->
+                Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+                  (i, i0) ntable0.hashmap_hash_map_max_load
+                  ntable0.hashmap_hash_map_slots)
+              end
             end
           end
-        end
-      else
-        Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
-          self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+        else
+          Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i,
+            i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+      end
     end
   end
 
@@ -304,18 +307,11 @@ let hashmap_hash_map_insert_fwd_back
     | Return i ->
       if i > self0.hashmap_hash_map_max_load
       then
-        begin match
-          hashmap_hash_map_try_resize_fwd_back t (Mkhashmap_hash_map_t
-            self0.hashmap_hash_map_num_entries
-            self0.hashmap_hash_map_max_load_factor
-            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) with
+        begin match hashmap_hash_map_try_resize_fwd_back t self0 with
         | Fail -> Fail
         | Return self1 -> Return self1
         end
-      else
-        Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
-          self0.hashmap_hash_map_max_load_factor
-          self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+      else Return self0
     end
   end
 
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
 /// The scalar types
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index aafc0cf6..874b739c 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
   | Return (st0, _) ->
     begin match swap_back u32 x 0 st with
     | Fail -> Fail
-    | Return (x0, _) ->
-      begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end
+    | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0)
     end
   end
 
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 97688191..35d32514 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -56,10 +56,14 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 =
 
 (** [no_nested_borrows::cast_test] *)
 let cast_test_fwd (x : u32) : result i32 =
-  begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end
+  begin match scalar_cast U32 I32 x with
+  | Fail -> Fail
+  | Return i -> Return i
+  end
 
 (** [no_nested_borrows::test2] *)
-let test2_fwd : result unit = Return ()
+let test2_fwd : result unit =
+  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -87,7 +91,11 @@ let test3_fwd : result unit =
 let _ = assert_norm (test3_fwd = Return ())
 
 (** [no_nested_borrows::test_neg1] *)
-let test_neg1_fwd : result unit = Return ()
+let test_neg1_fwd : result unit =
+  begin match i32_neg 3 with
+  | Fail -> Fail
+  | Return y -> if not (y = -3) then Fail else Return ()
+  end
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
@@ -222,27 +230,25 @@ and node_elem_t (t : Type0) =
 
 (** [no_nested_borrows::even] *)
 let rec even_fwd (x : u32) : result bool =
-  begin match x with
-  | 0 -> Return true
-  | _ ->
+  if x = 0
+  then Return true
+  else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
       begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
     end
-  end
 
 (** [no_nested_borrows::odd] *)
 and odd_fwd (x : u32) : result bool =
-  begin match x with
-  | 0 -> Return false
-  | _ ->
+  if x = 0
+  then Return false
+  else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
       begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
     end
-  end
 
 (** [no_nested_borrows::test_even_odd] *)
 let test_even_odd_fwd : result unit =
@@ -291,9 +297,9 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
 let rec list_nth_shared_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 ->
@@ -302,7 +308,6 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
         | Return x0 -> Return x0
         end
       end
-    end
   | ListNil -> Fail
   end
 
@@ -310,9 +315,9 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
 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 ->
@@ -321,7 +326,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
 
@@ -330,9 +334,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 ->
@@ -341,7 +345,6 @@ let rec list_nth_mut_back
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-    end
   | ListNil -> Fail
   end
 
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
 
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
 /// The scalar types