diff options
author | Son Ho | 2022-05-06 10:27:35 +0200 |
---|---|---|
committer | Son Ho | 2022-05-06 10:27:35 +0200 |
commit | 3a561145197762da371f4c32d2c47953e3d1afcd (patch) | |
tree | f6de68aeee31093308604ca2b3ece89c0a20c8ba /tests/misc | |
parent | a593c7638c9c675425a7a03f0981a1f19881be11 (diff) |
Regenerate the F* files for external.rs
Diffstat (limited to 'tests/misc')
-rw-r--r-- | tests/misc/External.Funs.fst | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst index 3025da55..0ad40b00 100644 --- a/tests/misc/External.Funs.fst +++ b/tests/misc/External.Funs.fst @@ -11,7 +11,15 @@ include External.Opaque let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = begin match core_mem_swap_fwd t x y st with | Fail -> Fail - | Return (st0, _) -> Return (st0, ()) + | Return (st0, _) -> + begin match core_mem_swap_back0 t x y st with + | Fail -> Fail + | Return _ -> + begin match core_mem_swap_back1 t x y st with + | Fail -> Fail + | Return _ -> Return (st0, ()) + end + end end (** [external::swap] *) @@ -58,7 +66,11 @@ let custom_swap_fwd | Return (st0, _) -> begin match core_mem_swap_back0 t x y st with | Fail -> Fail - | Return x0 -> Return (st0, x0) + | Return x0 -> + begin match core_mem_swap_back1 t x y st with + | Fail -> Fail + | Return _ -> Return (st0, x0) + end end end |