diff options
Diffstat (limited to 'tests/fstar/betree')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index f6045dfd..f4ba7927 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -1139,8 +1139,8 @@ let rec betree_node_apply_messages_fwd (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (state & unit)) - (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs - st)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) = begin match self with | BetreeNodeInternal node -> @@ -1229,8 +1229,8 @@ and betree_node_apply_messages_back (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (betree_node_t & betree_node_id_counter_t)) - (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs - st)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) = begin match self with | BetreeNodeInternal node -> @@ -1329,8 +1329,8 @@ and betree_internal_flush_fwd (node_id_cnt : betree_node_id_counter_t) (content : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (state & (betree_list_t (u64 & betree_message_t)))) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) = begin match betree_list_partition_at_pivot_fwd betree_message_t content @@ -1397,8 +1397,8 @@ and betree_internal_flush_back (node_id_cnt : betree_node_id_counter_t) (content : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (betree_internal_t & betree_node_id_counter_t)) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) = begin match betree_list_partition_at_pivot_fwd betree_message_t content |