diff options
| author | Son Ho | 2022-11-15 15:23:16 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-16 15:45:32 +0100 |
| commit | bd5706896dec0a1aef1accdf51f93af00c5dc6fe (patch) | |
| tree | 09dd5431d351c8ef894092ea25fd9d2af54d3d6e /tests/fstar/betree | |
| parent | dbb5d549176edd60440e689fd28c529944bc6e51 (diff) | |
Improve formatting
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 |