summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/misc/External.Funs.fst19
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
+