Regenerate the F* files for external.rs

1 files changed, 17 insertions, 2 deletions

diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 21a389ca..3025da55 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -40,13 +40,16 @@ let test_new_non_zero_u32_fwd
   end
 
 (** [external::test_vec] *)
-let test_vec_fwd (st : state) : result (state & unit) =
+let test_vec_fwd : result unit =
   let v = vec_new u32 in
   begin match vec_push_back u32 v 0 with
   | Fail -> Fail
-  | Return _ -> Return (st, ())
+  | Return _ -> Return ()
   end
 
+(** Unit test for [external::test_vec] *)
+let _ = assert_norm (test_vec_fwd = Return ())
+
 (** [external::custom_swap] *)
 let custom_swap_fwd
   (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
@@ -87,3 +90,15 @@ let test_custom_swap_back
   | Return (x0, y0) -> Return (x0, y0)
   end
 
+(** [external::test_swap_non_zero] *)
+let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
+  begin match swap_fwd u32 x 0 st with
+  | Fail -> Fail
+  | 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
+    end
+  end
+