Make sure let-bindings in Lean end with line breaks and improve formatting

5 files changed, 116 insertions, 102 deletions

diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 1a2f4133..bf13ad43 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -22,14 +22,16 @@ let x2_body : result u32 = Return 3
 let x2_c : u32 = eval_global x2_body
 
 (** [constants::incr] *)
-let incr_fwd (n : u32) : result u32 = u32_add n 1
+let incr_fwd (n : u32) : result u32 =
+  u32_add n 1
 
 (** [constants::X3] *)
 let x3_body : result u32 = incr_fwd 32
 let x3_c : u32 = eval_global x3_body
 
 (** [constants::mk_pair0] *)
-let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) =
+  Return (x, y)
 
 (** [constants::Pair] *)
 type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
@@ -66,7 +68,8 @@ let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
 let y_c : wrap_t i32 = eval_global y_body
 
 (** [constants::unwrap_y] *)
-let unwrap_y_fwd : result i32 = Return y_c.wrap_val
+let unwrap_y_fwd : result i32 =
+  Return y_c.wrap_val
 
 (** [constants::YVAL] *)
 let yval_body : result i32 = unwrap_y_fwd
@@ -77,10 +80,12 @@ let get_z1_z1_body : result i32 = Return 3
 let get_z1_z1_c : i32 = eval_global get_z1_z1_body
 
 (** [constants::get_z1] *)
-let get_z1_fwd : result i32 = Return get_z1_z1_c
+let get_z1_fwd : result i32 =
+  Return get_z1_z1_c
 
 (** [constants::add] *)
-let add_fwd (a : i32) (b : i32) : result i32 = i32_add a b
+let add_fwd (a : i32) (b : i32) : result i32 =
+  i32_add a b
 
 (** [constants::Q1] *)
 let q1_body : result i32 = Return 5
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 0d3c39f7..7fe175e5 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -13,13 +13,12 @@ let rec sum_loop_fwd
   Tot (result u32) (decreases (sum_loop_decreases max i s))
   =
   if i < max
-  then begin
-    let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0
-    end
+  then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0
   else u32_mul s 2
 
 (** [loops::sum] *)
-let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
+let sum_fwd (max : u32) : result u32 =
+  sum_loop_fwd max 0 0
 
 (** [loops::sum_with_mut_borrows] *)
 let rec sum_with_mut_borrows_loop_fwd
@@ -27,10 +26,10 @@ let rec sum_with_mut_borrows_loop_fwd
   Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms))
   =
   if mi < max
-  then begin
+  then
     let* ms0 = u32_add ms mi in
     let* mi0 = u32_add mi 1 in
-    sum_with_mut_borrows_loop_fwd max mi0 ms0 end
+    sum_with_mut_borrows_loop_fwd max mi0 ms0
   else u32_mul ms 2
 
 (** [loops::sum_with_mut_borrows] *)
@@ -43,10 +42,10 @@ let rec sum_with_shared_borrows_loop_fwd
   Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s))
   =
   if i < max
-  then begin
+  then
     let* i0 = u32_add i 1 in
     let* s0 = u32_add s i0 in
-    sum_with_shared_borrows_loop_fwd max i0 s0 end
+    sum_with_shared_borrows_loop_fwd max i0 s0
   else u32_mul s 2
 
 (** [loops::sum_with_shared_borrows] *)
@@ -60,14 +59,15 @@ let rec clear_loop_fwd_back
   =
   let i0 = vec_len u32 v in
   if i < i0
-  then begin
+  then
     let* i1 = usize_add i 1 in
     let* v0 = vec_index_mut_back u32 v i 0 in
-    clear_loop_fwd_back v0 i1 end
+    clear_loop_fwd_back v0 i1
   else Return v
 
 (** [loops::clear] *)
-let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0
+let clear_fwd_back (v : vec u32) : result (vec u32) =
+  clear_loop_fwd_back v 0
 
 (** [loops::list_mem] *)
 let rec list_mem_loop_fwd
@@ -92,7 +92,7 @@ let rec list_nth_mut_loop_loop_fwd
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 end
+    else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0
   | ListNil -> Fail Failure
   end
 
@@ -109,10 +109,10 @@ let rec list_nth_mut_loop_loop_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else begin
+    else
       let* i0 = u32_sub i 1 in
       let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in
-      Return (ListCons x tl0) end
+      Return (ListCons x tl0)
   | ListNil -> Fail Failure
   end
 
@@ -130,8 +130,7 @@ let rec list_nth_shared_loop_loop_fwd
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0
-      end
+    else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0
   | ListNil -> Fail Failure
   end
 
@@ -163,8 +162,7 @@ let rec get_elem_mut_loop_back
   | ListCons y tl ->
     if y = x
     then Return (ListCons ret tl)
-    else begin
-      let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) end
+    else let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0)
   | ListNil -> Fail Failure
   end
 
@@ -193,7 +191,8 @@ let get_elem_shared_fwd
   let* l = vec_index_fwd (list_t usize) slots 0 in get_elem_shared_loop_fwd x l
 
 (** [loops::id_mut] *)
-let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
+let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) =
+  Return ls
 
 (** [loops::id_mut] *)
 let id_mut_back
@@ -201,7 +200,8 @@ let id_mut_back
   Return ret
 
 (** [loops::id_shared] *)
-let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
+let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) =
+  Return ls
 
 (** [loops::list_nth_mut_loop_with_id] *)
 let rec list_nth_mut_loop_with_id_loop_fwd
@@ -212,8 +212,7 @@ let rec list_nth_mut_loop_with_id_loop_fwd
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin
-      let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl end
+    else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl
   | ListNil -> Fail Failure
   end
 
@@ -232,10 +231,10 @@ let rec list_nth_mut_loop_with_id_loop_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else begin
+    else
       let* i0 = u32_sub i 1 in
       let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in
-      Return (ListCons x tl0) end
+      Return (ListCons x tl0)
   | ListNil -> Fail Failure
   end
 
@@ -256,9 +255,7 @@ let rec list_nth_shared_loop_with_id_loop_fwd
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin
-      let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl
-      end
+    else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl
   | ListNil -> Fail Failure
   end
 
@@ -280,9 +277,8 @@ let rec list_nth_mut_loop_pair_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0
-        end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -305,10 +301,10 @@ let rec list_nth_mut_loop_pair_loop_back'a
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in
-        Return (ListCons x0 tl00) end
+        Return (ListCons x0 tl00)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -333,10 +329,10 @@ let rec list_nth_mut_loop_pair_loop_back'b
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in
-        Return (ListCons x1 tl10) end
+        Return (ListCons x1 tl10)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -361,9 +357,9 @@ let rec list_nth_shared_loop_pair_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 end
+        list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -386,9 +382,9 @@ let rec list_nth_mut_loop_pair_merge_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
+        list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -411,11 +407,11 @@ let rec list_nth_mut_loop_pair_merge_loop_back
     | ListCons x1 tl1 ->
       if i = 0
       then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* (tl00, tl10) =
           list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
-        Return (ListCons x0 tl00, ListCons x1 tl10) end
+        Return (ListCons x0 tl00, ListCons x1 tl10)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -440,9 +436,9 @@ let rec list_nth_shared_loop_pair_merge_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
+        list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -465,9 +461,9 @@ let rec list_nth_mut_shared_loop_pair_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 end
+        list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -490,10 +486,10 @@ let rec list_nth_mut_shared_loop_pair_loop_back
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in
-        Return (ListCons x0 tl00) end
+        Return (ListCons x0 tl00)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -518,9 +514,9 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
+        list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -543,11 +539,11 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl00 =
           list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
-        Return (ListCons x0 tl00) end
+        Return (ListCons x0 tl00)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -572,9 +568,9 @@ let rec list_nth_shared_mut_loop_pair_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 end
+        list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -597,10 +593,10 @@ let rec list_nth_shared_mut_loop_pair_loop_back
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in
-        Return (ListCons x1 tl10) end
+        Return (ListCons x1 tl10)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -625,9 +621,9 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
-        list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
+        list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -650,11 +646,11 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
-      else begin
+      else
         let* i0 = u32_sub i 1 in
         let* tl10 =
           list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
-        Return (ListCons x1 tl10) end
+        Return (ListCons x1 tl10)
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index ce1f544c..1e186c79 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -31,28 +31,36 @@ type sum_t (t1 t2 : Type0) =
 | SumRight : t2 -> sum_t t1 t2
 
 (** [no_nested_borrows::neg_test] *)
-let neg_test_fwd (x : i32) : result i32 = i32_neg x
+let neg_test_fwd (x : i32) : result i32 =
+  i32_neg x
 
 (** [no_nested_borrows::add_test] *)
-let add_test_fwd (x : u32) (y : u32) : result u32 = u32_add x y
+let add_test_fwd (x : u32) (y : u32) : result u32 =
+  u32_add x y
 
 (** [no_nested_borrows::subs_test] *)
-let subs_test_fwd (x : u32) (y : u32) : result u32 = u32_sub x y
+let subs_test_fwd (x : u32) (y : u32) : result u32 =
+  u32_sub x y
 
 (** [no_nested_borrows::div_test] *)
-let div_test_fwd (x : u32) (y : u32) : result u32 = u32_div x y
+let div_test_fwd (x : u32) (y : u32) : result u32 =
+  u32_div x y
 
 (** [no_nested_borrows::div_test1] *)
-let div_test1_fwd (x : u32) : result u32 = u32_div x 2
+let div_test1_fwd (x : u32) : result u32 =
+  u32_div x 2
 
 (** [no_nested_borrows::rem_test] *)
-let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y
+let rem_test_fwd (x : u32) (y : u32) : result u32 =
+  u32_rem x y
 
 (** [no_nested_borrows::cast_test] *)
-let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x
+let cast_test_fwd (x : u32) : result i32 =
+  scalar_cast U32 I32 x
 
 (** [no_nested_borrows::test2] *)
-let test2_fwd : result unit = let* _ = u32_add 23 44 in Return ()
+let test2_fwd : result unit =
+  let* _ = u32_add 23 44 in Return ()
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -101,7 +109,8 @@ let refs_test2_fwd : result unit =
 let _ = assert_norm (refs_test2_fwd = Return ())
 
 (** [no_nested_borrows::test_list1] *)
-let test_list1_fwd : result unit = Return ()
+let test_list1_fwd : result unit =
+  Return ()
 
 (** Unit test for [no_nested_borrows::test_list1] *)
 let _ = assert_norm (test_list1_fwd = Return ())
@@ -114,7 +123,8 @@ let test_box1_fwd : result unit =
 let _ = assert_norm (test_box1_fwd = Return ())
 
 (** [no_nested_borrows::copy_int] *)
-let copy_int_fwd (x : i32) : result i32 = Return x
+let copy_int_fwd (x : i32) : result i32 =
+  Return x
 
 (** [no_nested_borrows::test_unreachable] *)
 let test_unreachable_fwd (b : bool) : result unit =
@@ -179,17 +189,18 @@ let choose_test_fwd : result unit =
   let* z0 = i32_add z 1 in
   if not (z0 = 1)
   then Fail Failure
-  else begin
+  else
     let* (x, y) = choose_back i32 true 0 0 z0 in
     if not (x = 1)
     then Fail Failure
-    else if not (y = 0) then Fail Failure else Return () end
+    else if not (y = 0) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::choose_test] *)
 let _ = assert_norm (choose_test_fwd = Return ())
 
 (** [no_nested_borrows::test_char] *)
-let test_char_fwd : result char = Return 'a'
+let test_char_fwd : result char =
+  Return 'a'
 
 (** [no_nested_borrows::NodeElem] *)
 type node_elem_t (t : Type0) =
@@ -214,7 +225,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0 end
+    else let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0
   | ListNil -> Fail Failure
   end
 
@@ -224,7 +235,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end
+    else let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0
   | ListNil -> Fail Failure
   end
 
@@ -235,10 +246,10 @@ let rec list_nth_mut_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else begin
+    else
       let* i0 = u32_sub i 1 in
       let* tl0 = list_nth_mut_back t tl i0 ret in
-      Return (ListCons x tl0) end
+      Return (ListCons x tl0)
   | ListNil -> Fail Failure
   end
 
@@ -263,31 +274,30 @@ let test_list_functions_fwd : result unit =
   let* i = list_length_fwd i32 (ListCons 0 l1) in
   if not (i = 3)
   then Fail Failure
-  else begin
+  else
     let* i0 = list_nth_shared_fwd i32 (ListCons 0 l1) 0 in
     if not (i0 = 0)
     then Fail Failure
-    else begin
+    else
       let* i1 = list_nth_shared_fwd i32 (ListCons 0 l1) 1 in
       if not (i1 = 1)
       then Fail Failure
-      else begin
+      else
         let* i2 = list_nth_shared_fwd i32 (ListCons 0 l1) 2 in
         if not (i2 = 2)
         then Fail Failure
-        else begin
+        else
           let* ls = list_nth_mut_back i32 (ListCons 0 l1) 1 3 in
           let* i3 = list_nth_shared_fwd i32 ls 0 in
           if not (i3 = 0)
           then Fail Failure
-          else begin
+          else
             let* i4 = list_nth_shared_fwd i32 ls 1 in
             if not (i4 = 3)
             then Fail Failure
-            else begin
+            else
               let* i5 = list_nth_shared_fwd i32 ls 2 in
-              if not (i5 = 2) then Fail Failure else Return () end end end end
-      end end
+              if not (i5 = 2) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
 let _ = assert_norm (test_list_functions_fwd = Return ())
@@ -369,27 +379,28 @@ let test_constants_fwd : result unit =
   let (i, _) = swt.struct_with_tuple_p in
   if not (i = 1)
   then Fail Failure
-  else begin
+  else
     let* swt0 = new_tuple2_fwd in
     let (i0, _) = swt0.struct_with_tuple_p in
     if not (i0 = 1)
     then Fail Failure
-    else begin
+    else
       let* swt1 = new_tuple3_fwd in
       let (i1, _) = swt1.struct_with_tuple_p in
       if not (i1 = 1)
       then Fail Failure
-      else begin
+      else
         let* swp = new_pair1_fwd in
         if not (swp.struct_with_pair_p.pair_x = 1)
         then Fail Failure
-        else Return () end end end
+        else Return ()
 
 (** Unit test for [no_nested_borrows::test_constants] *)
 let _ = assert_norm (test_constants_fwd = Return ())
 
 (** [no_nested_borrows::test_weird_borrows1] *)
-let test_weird_borrows1_fwd : result unit = Return ()
+let test_weird_borrows1_fwd : result unit =
+  Return ()
 
 (** Unit test for [no_nested_borrows::test_weird_borrows1] *)
 let _ = assert_norm (test_weird_borrows1_fwd = Return ())
@@ -404,12 +415,14 @@ let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
   if b then Return 0 else Return 1
 
 (** [no_nested_borrows::test_shared_borrow_bool2] *)
-let test_shared_borrow_bool2_fwd : result u32 = Return 0
+let test_shared_borrow_bool2_fwd : result u32 =
+  Return 0
 
 (** [no_nested_borrows::test_shared_borrow_enum1] *)
 let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 =
   begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end
 
 (** [no_nested_borrows::test_shared_borrow_enum2] *)
-let test_shared_borrow_enum2_fwd : result u32 = Return 0
+let test_shared_borrow_enum2_fwd : result u32 =
+  Return 0
 
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 95f13f62..4ab31de3 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -6,7 +6,8 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [paper::ref_incr] *)
-let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1
+let ref_incr_fwd_back (x : i32) : result i32 =
+  i32_add x 1
 
 (** [paper::test_incr] *)
 let test_incr_fwd : result unit =
@@ -31,11 +32,11 @@ let test_choose_fwd : result unit =
   let* z0 = i32_add z 1 in
   if not (z0 = 1)
   then Fail Failure
-  else begin
+  else
     let* (x, y) = choose_back i32 true 0 0 z0 in
     if not (x = 1)
     then Fail Failure
-    else if not (y = 0) then Fail Failure else Return () end
+    else if not (y = 0) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_choose] *)
 let _ = assert_norm (test_choose_fwd = Return ())
@@ -51,7 +52,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | ListCons x tl ->
     if i = 0
     then Return x
-    else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end
+    else let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0
   | ListNil -> Fail Failure
   end
 
@@ -62,10 +63,10 @@ let rec list_nth_mut_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else begin
+    else
       let* i0 = u32_sub i 1 in
       let* tl0 = list_nth_mut_back t tl i0 ret in
-      Return (ListCons x tl0) end
+      Return (ListCons x tl0)
   | ListNil -> Fail Failure
   end
 
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index db0dc0d5..e2144487 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -25,8 +25,7 @@ let rec get_list_at_x_back
   | ListCons hd tl ->
     if hd = x
     then Return ret
-    else begin
-      let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) end
+    else let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0)
   | ListNil -> Return ret
   end