diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 6 | ||||
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 11 |
2 files changed, 8 insertions, 9 deletions
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index f75a0c01..4fb9c8e4 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -181,8 +181,7 @@ let hash_map_insert_no_resize_fwd_back | Fail -> Fail | Return v -> Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load - v) + self.hash_map_max_load_factor self.hash_map_max_load v) end end end @@ -574,8 +573,7 @@ let hash_map_remove_back | Fail -> Fail | Return v -> Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load - v) + self.hash_map_max_load_factor self.hash_map_max_load v) end end | Some x0 -> diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index 8620f7e9..2a06fd76 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -341,10 +341,10 @@ let rec list_nth_mut_back (** [no_nested_borrows::list_rev_aux] *) let rec list_rev_aux_fwd - (t : Type0) (lo : list_t t) (li : list_t t) : result (list_t t) = + (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) = begin match li with | ListCons hd tl -> - begin match list_rev_aux_fwd t (ListCons hd lo) tl with + begin match list_rev_aux_fwd t tl (ListCons hd lo) with | Fail -> Fail | Return l -> Return l end @@ -354,7 +354,7 @@ let rec list_rev_aux_fwd (** [no_nested_borrows::list_rev] *) let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) = let li = mem_replace_fwd (list_t t) l ListNil in - begin match list_rev_aux_fwd t ListNil li with + begin match list_rev_aux_fwd t li ListNil with | Fail -> Fail | Return l0 -> Return l0 end @@ -516,8 +516,9 @@ let test_constants_fwd : result unit = begin match new_pair1_fwd with | Fail -> Fail | Return swp -> - let p = swp.struct_with_pair_p in - if not (p.pair_x = 1) then Fail else Return () + if not (swp.struct_with_pair_p.pair_x = 1) + then Fail + else Return () end end end |