diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 38be12ac..2aca9fbe 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -158,7 +158,7 @@ let hashMap_move_elements_from_list let rec hashMap_move_elements_loop (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t)) (i : usize) : - Tot (result ((alloc_vec_Vec (list_t t)) & (hashMap_t t))) + Tot (result ((hashMap_t t) & (alloc_vec_Vec (list_t t)))) (decreases (hashMap_move_elements_loop_decreases t ntable slots i)) = let i1 = alloc_vec_Vec_len (list_t t) slots in diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index cf3ae858..4a032207 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -167,7 +167,7 @@ let hashmap_HashMap_move_elements_from_list let rec hashmap_HashMap_move_elements_loop (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : - Tot (result ((alloc_vec_Vec (hashmap_List_t t)) & (hashmap_HashMap_t t))) + Tot (result ((hashmap_HashMap_t t) & (alloc_vec_Vec (hashmap_List_t t)))) (decreases (hashmap_HashMap_move_elements_loop_decreases t ntable slots i)) = let i1 = alloc_vec_Vec_len (hashmap_List_t t) slots in |