From bd5706896dec0a1aef1accdf51f93af00c5dc6fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 15 Nov 2022 15:23:16 +0100
Subject: Improve formatting

---
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 30 ++++++++++++----------
 1 file changed, 16 insertions(+), 14 deletions(-)

(limited to 'tests/fstar/betree_back_stateful/BetreeMain.Funs.fst')

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 6a2b7c09..1560624b 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -1222,8 +1222,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 ->
@@ -1318,8 +1318,8 @@ and betree_node_apply_messages_back'a
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
   Tot (result (state & (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 ->
@@ -1425,8 +1425,8 @@ and betree_node_apply_messages_back1
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : 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 ->
@@ -1533,8 +1533,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
@@ -1619,10 +1619,11 @@ and betree_internal_flush_fwd
 and betree_internal_flush_back'a
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
+  :
   Tot (result (state & (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
@@ -1716,10 +1717,11 @@ and betree_internal_flush_back'a
 and betree_internal_flush_back1
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
+  :
   Tot (result (state & unit))
-  (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
-- 
cgit v1.2.3