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

25 files changed, 446 insertions, 377 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a995ee7f..4c23989e 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1756,8 +1756,13 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
 and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (e : texpression) : unit =
   let lets, next_e = destruct_lets e in
-  (* Open a box for the whole expression *)
-  F.pp_open_hvbox fmt 0;
+  (* Open a box for the whole expression.
+
+     In the case of Lean, we use a vbox so that line breaks are inserted
+     at the end of every let-binding: let-bindings are indeed not ended
+     with an "in" keyword.
+  *)
+  if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
   (* Open parentheses *)
   if inside && !backend <> Lean then F.pp_print_string fmt "(";
   (* Extract the let-bindings *)
@@ -1804,12 +1809,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
         extract_texpression ctx fmt false re;
-        (* In Lean, monadic let-bindings don't require to end with "in".
-
-           TODO: does this work because we add a line break? This is very annoying,
-           because we need to enforce there will be a line break. In order to fix
-           this, we should open a vbox instead of an hov_box.
-        *)
+        (* In Lean, monadic let-bindings don't require to end with "in" *)
         if !backend <> Lean then (
           F.pp_print_space fmt ();
           F.pp_print_string fmt "in");
@@ -1855,51 +1855,54 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   (* Extract the switch *)
   (match body with
   | If (e_then, e_else) ->
-      (* Open a box for the [if] *)
+      (* Open a box for the [if e] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       F.pp_print_string fmt "if";
       F.pp_print_space fmt ();
-      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
+      let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
-      (* Close the box for the [if] *)
+      (* Close the box for the [if e] *)
       F.pp_close_box fmt ();
       (* Extract the branches *)
       let extract_branch (is_then : bool) (e_branch : texpression) : unit =
         F.pp_print_space fmt ();
         (* Open a box for the then/else+branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
+        F.pp_open_hvbox fmt ctx.indent_incr;
+        (* Open a box for the then/else + space + opening parenthesis *)
+        F.pp_open_hovbox fmt 0;
         let then_or_else = if is_then then "then" else "else" in
         F.pp_print_string fmt then_or_else;
-        let parenth = PureUtils.let_group_requires_parentheses e_branch in
-        (* Open a box for the branch - we do this only if it is not a parenthesized
-           group of nested let bindings.
-        *)
-        if not parenth then (
-          F.pp_print_space fmt ();
-          F.pp_open_hovbox fmt ctx.indent_incr);
+        let parenth = PureUtils.texpression_requires_parentheses e_branch in
         (* Open the parenthesized expression *)
-        (if parenth then
-         match !backend with
-         | FStar ->
-             F.pp_print_space fmt ();
-             F.pp_print_string fmt "begin";
-             F.pp_print_space fmt ()
-         | Coq ->
-             F.pp_print_string fmt " (";
-             F.pp_print_cut fmt ()
-         | Lean -> F.pp_print_cut fmt ());
+        let print_space_after_parenth =
+          if parenth then (
+            match !backend with
+            | FStar ->
+                F.pp_print_space fmt ();
+                F.pp_print_string fmt "begin";
+                F.pp_print_space fmt
+            | Coq | Lean ->
+                F.pp_print_space fmt ();
+                F.pp_print_string fmt "(";
+                F.pp_print_cut fmt)
+          else F.pp_print_space fmt
+        in
+        (* Close the box for the then/else + space + opening parenthesis *)
+        F.pp_close_box fmt ();
+        print_space_after_parenth ();
+        (* Open a box for the branch *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the branch expression *)
         extract_texpression ctx fmt false e_branch;
+        (* Close the box for the branch *)
+        F.pp_close_box fmt ();
         (* Close the parenthesized expression *)
         (if parenth then
          match !backend with
          | FStar ->
              F.pp_print_space fmt ();
              F.pp_print_string fmt "end"
-         | Coq -> F.pp_print_string fmt ")"
-         | Lean -> ());
-        (* Close the box for the branch *)
-        if not parenth then F.pp_close_box fmt ();
+         | Coq | Lean -> F.pp_print_string fmt ")");
         (* Close the box for the then/else+branch *)
         F.pp_close_box fmt ()
       in
@@ -1915,7 +1918,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       in
       F.pp_print_string fmt match_begin;
       F.pp_print_space fmt ();
-      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
+      let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
       F.pp_print_string fmt "with";
@@ -1926,14 +1929,18 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       let extract_branch (br : match_branch) : unit =
         F.pp_print_space fmt ();
         (* Open a box for the pattern+branch *)
+        F.pp_open_hvbox fmt ctx.indent_incr;
+        (* Open a box for the pattern *)
         F.pp_open_hovbox fmt ctx.indent_incr;
-        F.pp_print_string fmt "|";
         (* Print the pattern *)
+        F.pp_print_string fmt "|";
         F.pp_print_space fmt ();
         let ctx = extract_typed_pattern ctx fmt false br.pat in
         F.pp_print_space fmt ();
         let arrow = match !backend with FStar -> "->" | Coq | Lean -> "=>" in
         F.pp_print_string fmt arrow;
+        (* Close the box for the pattern *)
+        F.pp_close_box fmt ();
         F.pp_print_space fmt ();
         (* Open a box for the branch *)
         F.pp_open_hovbox fmt ctx.indent_incr;
@@ -2228,7 +2235,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open two boxes for the definition, so that whenever possible it gets printed on
    * one line and indents are correct *)
   F.pp_open_hvbox fmt 0;
-  F.pp_open_hvbox fmt ctx.indent_incr;
+  F.pp_open_vbox fmt ctx.indent_incr;
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
@@ -2379,7 +2386,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       ctx_get_terminates_clause def.def_id def.loop_id ctx
     in
     F.pp_print_break fmt 0 0;
-    (* Open a box for the whole {terminates_by CALL => DECREASES } *)
+    (* Open a box for the whole [terminates_by CALL => DECREASES] *)
     F.pp_open_hvbox fmt ctx.indent_incr;
     (* Open a box for {terminates_by CALL =>} *)
     F.pp_open_hovbox fmt ctx.indent_incr;
@@ -2393,10 +2400,10 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       all_vars;
     F.pp_print_space fmt ();
     F.pp_print_string fmt "=>";
-    (* Close the box for {terminates_by CALL =>} *)
+    (* Close the box for [terminates_by CALL =>] *)
     F.pp_close_box fmt ();
     F.pp_print_space fmt ();
-    (* Open the box for {DECREASES} *)
+    (* Open the box for [DECREASES] *)
     F.pp_open_hovbox fmt ctx.indent_incr;
     F.pp_print_string fmt terminates_name;
     List.iter
@@ -2410,9 +2417,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt (ctx_get_var v ctx_body))
       vars;
-    (* Close the box for {DECREASES} *)
+    (* Close the box for [DECREASES] *)
     F.pp_close_box fmt ();
-    (* Close the box for the whole {terminates_by CALL => DECREASES } *)
+    (* Close the box for the whole [terminates_by CALL => DECREASES] *)
     F.pp_close_box fmt ();
 
     let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e13743c4..40005671 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -152,8 +152,8 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
     We only look for outer monadic let-bindings.
     This is used when printing the branches of [if ... then ... else ...].
 
-    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop} nodes (you should call
-    it on an expression where those nodes have been eliminated).
+    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop}
+    nodes (you should call it on an expression where those nodes have been eliminated).
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
@@ -166,6 +166,11 @@ let rec let_group_requires_parentheses (e : texpression) : bool =
       (* Should have been eliminated *)
       raise (Failure "Unreachable")
 
+let texpression_requires_parentheses e =
+  match !Config.backend with
+  | FStar | Lean -> false
+  | Coq -> let_group_requires_parentheses e
+
 let is_var (e : texpression) : bool =
   match e.e with Var _ -> true | _ -> false
 
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 10cdedd1..fe22b029 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -1156,6 +1156,7 @@ Definition betree_be_tree_lookup_back
 .
 
 (** [betree_main::main] *)
-Definition main_fwd : result unit := Return tt.
+Definition main_fwd : result unit :=
+  Return tt.
 
 End BetreeMain_Funs .
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 42c62421..e5a3f799 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,7 +3,7 @@
 -arg -w
 -arg all
 
-BetreeMain_Types.v
 Primitives.v
+BetreeMain_Types.v
 BetreeMain_Funs.v
 BetreeMain_Opaque.v
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index f1af0c21..b952e60c 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -9,7 +9,8 @@ Import Hashmap_Types.
 Module Hashmap_Funs.
 
 (** [hashmap::hash_key] *)
-Definition hash_key_fwd (k : usize) : result usize := Return k.
+Definition hash_key_fwd (k : usize) : result usize :=
+  Return k.
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hash_map_allocate_slots_loop_fwd
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index 7f80afbf..daa9b2ba 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -3,6 +3,6 @@
 -arg -w
 -arg all
 
-Hashmap_Types.v
 Primitives.v
+Hashmap_Types.v
 Hashmap_Funs.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 7c86dbe1..2a3ad87c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -11,7 +11,8 @@ Import HashmapMain_Opaque.
 Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key] *)
-Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
+Definition hashmap_hash_key_fwd (k : usize) : result usize :=
+  Return k.
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
@@ -598,7 +599,8 @@ Definition insert_on_disk_fwd
 .
 
 (** [hashmap_main::main] *)
-Definition main_fwd : result unit := Return tt.
+Definition main_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [hashmap_main::main] *)
 Check (main_fwd )%return.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index acc15a13..0a72558d 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -23,7 +23,8 @@ Definition x2_body : result u32 := Return (3%u32).
 Definition x2_c : u32 := x2_body%global.
 
 (** [constants::incr] *)
-Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32.
+Definition incr_fwd (n : u32) : result u32 :=
+  u32_add n 1%u32.
 
 (** [constants::X3] *)
 Definition x3_body : result u32 := incr_fwd (32%u32).
@@ -80,7 +81,8 @@ Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32).
 Definition y_c : Wrap_t i32 := y_body%global.
 
 (** [constants::unwrap_y] *)
-Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val).
+Definition unwrap_y_fwd : result i32 :=
+  Return y_c.(Wrap_val).
 
 (** [constants::YVAL] *)
 Definition yval_body : result i32 := unwrap_y_fwd.
@@ -91,10 +93,12 @@ Definition get_z1_z1_body : result i32 := Return (3%i32).
 Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
 
 (** [constants::get_z1] *)
-Definition get_z1_fwd : result i32 := Return get_z1_z1_c.
+Definition get_z1_fwd : result i32 :=
+  Return get_z1_z1_c.
 
 (** [constants::add] *)
-Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b.
+Definition add_fwd (a : i32) (b : i32) : result i32 :=
+  i32_add a b.
 
 (** [constants::Q1] *)
 Definition q1_body : result i32 := Return (5%i32).
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 10654887..98ed1cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -46,28 +46,36 @@ Arguments SumLeft {T1} {T2} _.
 Arguments SumRight {T1} {T2} _.
 
 (** [no_nested_borrows::neg_test] *)
-Definition neg_test_fwd (x : i32) : result i32 := i32_neg x.
+Definition neg_test_fwd (x : i32) : result i32 :=
+  i32_neg x.
 
 (** [no_nested_borrows::add_test] *)
-Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y.
+Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_add x y.
 
 (** [no_nested_borrows::subs_test] *)
-Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y.
+Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_sub x y.
 
 (** [no_nested_borrows::div_test] *)
-Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y.
+Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_div x y.
 
 (** [no_nested_borrows::div_test1] *)
-Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32.
+Definition div_test1_fwd (x : u32) : result u32 :=
+  u32_div x 2%u32.
 
 (** [no_nested_borrows::rem_test] *)
-Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
+Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_rem x y.
 
 (** [no_nested_borrows::cast_test] *)
-Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
+Definition cast_test_fwd (x : u32) : result i32 :=
+  scalar_cast U32 I32 x.
 
 (** [no_nested_borrows::test2] *)
-Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt.
+Definition test2_fwd : result unit :=
+  _ <- u32_add 23%u32 44%u32; Return tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2_fwd )%return.
@@ -122,7 +130,8 @@ Definition refs_test2_fwd : result unit :=
 Check (refs_test2_fwd )%return.
 
 (** [no_nested_borrows::test_list1] *)
-Definition test_list1_fwd : result unit := Return tt.
+Definition test_list1_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [no_nested_borrows::test_list1] *)
 Check (test_list1_fwd )%return.
@@ -138,7 +147,8 @@ Definition test_box1_fwd : result unit :=
 Check (test_box1_fwd )%return.
 
 (** [no_nested_borrows::copy_int] *)
-Definition copy_int_fwd (x : i32) : result i32 := Return x.
+Definition copy_int_fwd (x : i32) : result i32 :=
+  Return x.
 
 (** [no_nested_borrows::test_unreachable] *)
 Definition test_unreachable_fwd (b : bool) : result unit :=
@@ -468,7 +478,8 @@ Definition test_constants_fwd : result unit :=
 Check (test_constants_fwd )%return.
 
 (** [no_nested_borrows::test_weird_borrows1] *)
-Definition test_weird_borrows1_fwd : result unit := Return tt.
+Definition test_weird_borrows1_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [no_nested_borrows::test_weird_borrows1] *)
 Check (test_weird_borrows1_fwd )%return.
@@ -485,7 +496,8 @@ Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 :=
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool2] *)
-Definition test_shared_borrow_bool2_fwd : result u32 := Return (0%u32).
+Definition test_shared_borrow_bool2_fwd : result u32 :=
+  Return (0%u32).
 
 (** [no_nested_borrows::test_shared_borrow_enum1] *)
 Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
@@ -496,6 +508,7 @@ Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
 .
 
 (** [no_nested_borrows::test_shared_borrow_enum2] *)
-Definition test_shared_borrow_enum2_fwd : result u32 := Return (0%u32).
+Definition test_shared_borrow_enum2_fwd : result u32 :=
+  Return (0%u32).
 
 End NoNestedBorrows .
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index cb4486c6..8045222d 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -7,7 +7,8 @@ Local Open Scope Primitives_scope.
 Module Paper.
 
 (** [paper::ref_incr] *)
-Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32.
+Definition ref_incr_fwd_back (x : i32) : result i32 :=
+  i32_add x 1%i32.
 
 (** [paper::test_incr] *)
 Definition test_incr_fwd : result unit :=
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index db6c2742..87dea3e6 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,12 +3,12 @@
 -arg -w
 -arg all
 
-Loops.v
+Constants.v
+External_Types.v
 Primitives.v
+Loops.v
 External_Funs.v
-Constants.v
 PoloniusList.v
-External_Types.v
 NoNestedBorrows.v
 External_Opaque.v
 Paper.v
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 8c0c1cc1..f3a01884 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -41,7 +41,8 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   let* _ = u64_add counter 1 in Return counter
 
 (** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1
+let betree_fresh_node_id_back (counter : u64) : result u64 =
+  u64_add counter 1
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
@@ -161,11 +162,11 @@ let rec betree_list_partition_at_pivot_fwd
     let (i, x) = hd in
     if i >= pivot
     then Return (BetreeListNil, BetreeListCons (i, x) tl)
-    else begin
+    else
       let* p = betree_list_partition_at_pivot_fwd t tl pivot in
       let (ls0, ls1) = p in
       let l = ls0 in
-      Return (BetreeListCons (i, x) l, ls1) end
+      Return (BetreeListCons (i, x) l, ls1)
   | BetreeListNil -> Return (BetreeListNil, BetreeListNil)
   end
 
@@ -257,10 +258,10 @@ let rec betree_node_lookup_first_message_for_key_back
     let (i, m) = x in
     if i >= key
     then Return ret
-    else begin
+    else
       let* next_msgs0 =
         betree_node_lookup_first_message_for_key_back key next_msgs ret in
-      Return (BetreeListCons (i, m) next_msgs0) end
+      Return (BetreeListCons (i, m) next_msgs0)
   | BetreeListNil -> Return ret
   end
 
@@ -273,7 +274,7 @@ let rec betree_node_apply_upserts_fwd
   =
   let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
   if b
-  then begin
+  then
     let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
     let (_, m) = msg in
     begin match m with
@@ -283,13 +284,13 @@ let rec betree_node_apply_upserts_fwd
       let* v = betree_upsert_update_fwd prev s in
       let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in
       betree_node_apply_upserts_fwd msgs0 (Some v) key st
-    end end
-  else begin
+    end
+  else
     let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in
     let* _ =
       betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
         BetreeMessageInsert v) in
-    Return (st0, v) end
+    Return (st0, v)
 
 (** [betree_main::betree::Node::{5}::apply_upserts] *)
 let rec betree_node_apply_upserts_back
@@ -300,7 +301,7 @@ let rec betree_node_apply_upserts_back
   =
   let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
   if b
-  then begin
+  then
     let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
     let (_, m) = msg in
     begin match m with
@@ -310,11 +311,11 @@ let rec betree_node_apply_upserts_back
       let* v = betree_upsert_update_fwd prev s in
       let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in
       betree_node_apply_upserts_back msgs0 (Some v) key st
-    end end
-  else begin
+    end
+  else
     let* (_, v) = core_option_option_unwrap_fwd u64 prev st in
     betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-      BetreeMessageInsert v) end
+      BetreeMessageInsert v)
 
 (** [betree_main::betree::Node::{5}::lookup] *)
 let rec betree_node_lookup_fwd
@@ -331,13 +332,13 @@ let rec betree_node_lookup_fwd
     | BetreeListCons p l ->
       let (k, msg) = p in
       if k <> key
-      then begin
+      then
         let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0
           in
         let* _ =
           betree_node_lookup_first_message_for_key_back key msgs
             (BetreeListCons (k, msg) l) in
-        Return (st1, opt) end
+        Return (st1, opt)
       else
         begin match msg with
         | BetreeMessageInsert v ->
@@ -394,12 +395,12 @@ and betree_node_lookup_back
     | BetreeListCons p l ->
       let (k, msg) = p in
       if k <> key
-      then begin
+      then
         let* _ =
           betree_node_lookup_first_message_for_key_back key msgs
             (BetreeListCons (k, msg) l) in
         let* node0 = betree_internal_lookup_in_children_back node key st0 in
-        Return (BetreeNodeInternal node0) end
+        Return (BetreeNodeInternal node0)
       else
         begin match msg with
         | BetreeMessageInsert v ->
@@ -458,14 +459,14 @@ and betree_internal_lookup_in_children_back
   (decreases (betree_internal_lookup_in_children_decreases self key st))
   =
   if key < self.betree_internal_pivot
-  then begin
+  then
     let* n = betree_node_lookup_back self.betree_internal_left key st in
     Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right) end
-  else begin
+      self.betree_internal_pivot n self.betree_internal_right)
+  else
     let* n = betree_node_lookup_back self.betree_internal_right key st in
     Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n) end
+      self.betree_internal_pivot self.betree_internal_left n)
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -494,9 +495,9 @@ let rec betree_node_lookup_mut_in_bindings_back
     let (i, i0) = hd in
     if i >= key
     then Return ret
-    else begin
+    else
       let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0) end
+      Return (BetreeListCons (i, i0) tl0)
   | BetreeListNil -> Return ret
   end
 
@@ -509,7 +510,7 @@ let betree_node_apply_to_leaf_fwd_back
   let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
   let* b = betree_list_head_has_key_fwd u64 bindings0 key in
   if b
-  then begin
+  then
     let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
     begin match new_msg with
     | BetreeMessageInsert v ->
@@ -527,7 +528,7 @@ let betree_node_apply_to_leaf_fwd_back
       let* bindings2 =
         betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
       betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end end
+    end
   else
     begin match new_msg with
     | BetreeMessageInsert v ->
@@ -568,11 +569,11 @@ let rec betree_node_filter_messages_for_key_fwd_back
   | BetreeListCons p l ->
     let (k, m) = p in
     if k = key
-    then begin
+    then
       let* msgs0 =
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) in
-      betree_node_filter_messages_for_key_fwd_back key msgs0 end
+      betree_node_filter_messages_for_key_fwd_back key msgs0
     else Return (BetreeListCons (k, m) l)
   | BetreeListNil -> Return BetreeListNil
   end
@@ -603,10 +604,10 @@ let rec betree_node_lookup_first_message_after_key_back
   | BetreeListCons p next_msgs ->
     let (k, m) = p in
     if k = key
-    then begin
+    then
       let* next_msgs0 =
         betree_node_lookup_first_message_after_key_back key next_msgs ret in
-      Return (BetreeListCons (k, m) next_msgs0) end
+      Return (BetreeListCons (k, m) next_msgs0)
     else Return ret
   | BetreeListNil -> Return ret
   end
@@ -665,11 +666,11 @@ let betree_node_apply_to_internal_fwd_back
         betree_node_lookup_first_message_for_key_back key msgs msgs3
       end
     end
-  else begin
+  else
     let* msgs1 =
       betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
         new_msg) in
-    betree_node_lookup_first_message_for_key_back key msgs msgs1 end
+    betree_node_lookup_first_message_for_key_back key msgs msgs1
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
 let rec betree_node_apply_messages_to_internal_fwd_back
@@ -703,34 +704,34 @@ let rec betree_node_apply_messages_fwd
       betree_node_apply_messages_to_internal_fwd_back content msgs in
     let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
     if num_msgs >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st1, content1) =
         betree_internal_flush_fwd node params node_id_cnt content0 st0 in
       let* (node0, _) =
         betree_internal_flush_back node params node_id_cnt content0 st0 in
       let* (st2, _) =
         betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in
-      Return (st2, ()) end
-    else begin
+      Return (st2, ())
+    else
       let* (st1, _) =
         betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
-      Return (st1, ()) end
+      Return (st1, ())
   | BetreeNodeLeaf node ->
     let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
     let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
     let* len = betree_list_len_fwd (u64 & u64) content0 in
     let* i = u64_mul 2 params.betree_params_split_size in
     if len >= i
-    then begin
+    then
       let* (st1, _) =
         betree_leaf_split_fwd node content0 params node_id_cnt st0 in
       let* (st2, _) =
         betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
-      Return (st2, ()) end
-    else begin
+      Return (st2, ())
+    else
       let* (st1, _) =
         betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
-      Return (st1, ()) end
+      Return (st1, ())
   end
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
@@ -750,36 +751,36 @@ and betree_node_apply_messages_back
       betree_node_apply_messages_to_internal_fwd_back content msgs in
     let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
     if num_msgs >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st1, content1) =
         betree_internal_flush_fwd node params node_id_cnt content0 st0 in
       let* (node0, node_id_cnt0) =
         betree_internal_flush_back node params node_id_cnt content0 st0 in
       let* _ =
         betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in
-      Return (BetreeNodeInternal node0, node_id_cnt0) end
-    else begin
+      Return (BetreeNodeInternal node0, node_id_cnt0)
+    else
       let* _ =
         betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
-      Return (BetreeNodeInternal node, node_id_cnt) end
+      Return (BetreeNodeInternal node, node_id_cnt)
   | BetreeNodeLeaf node ->
     let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
     let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
     let* len = betree_list_len_fwd (u64 & u64) content0 in
     let* i = u64_mul 2 params.betree_params_split_size in
     if len >= i
-    then begin
+    then
       let* (st1, new_node) =
         betree_leaf_split_fwd node content0 params node_id_cnt st0 in
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1
         in
       let* node_id_cnt0 =
         betree_leaf_split_back node content0 params node_id_cnt st0 in
-      Return (BetreeNodeInternal new_node, node_id_cnt0) end
-    else begin
+      Return (BetreeNodeInternal new_node, node_id_cnt0)
+    else
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
       Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len),
-        node_id_cnt) end
+        node_id_cnt)
   end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
@@ -797,7 +798,7 @@ and betree_internal_flush_fwd
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
   if len_left >= params.betree_params_min_flush_size
-  then begin
+  then
     let* (st0, _) =
       betree_node_apply_messages_fwd self.betree_internal_left params
         node_id_cnt msgs_left st in
@@ -806,23 +807,23 @@ and betree_internal_flush_fwd
         node_id_cnt msgs_left st in
     let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
     if len_right >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st1, _) =
         betree_node_apply_messages_fwd self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
       let* _ =
         betree_node_apply_messages_back self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
-      Return (st1, BetreeListNil) end
-    else Return (st0, msgs_right) end
-  else begin
+      Return (st1, BetreeListNil)
+    else Return (st0, msgs_right)
+  else
     let* (st0, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
         node_id_cnt msgs_right st in
     let* _ =
       betree_node_apply_messages_back self.betree_internal_right params
         node_id_cnt msgs_right st in
-    Return (st0, msgs_left) end
+    Return (st0, msgs_left)
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back
@@ -839,7 +840,7 @@ and betree_internal_flush_back
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
   if len_left >= params.betree_params_min_flush_size
-  then begin
+  then
     let* (st0, _) =
       betree_node_apply_messages_fwd self.betree_internal_left params
         node_id_cnt msgs_left st in
@@ -848,22 +849,21 @@ and betree_internal_flush_back
         node_id_cnt msgs_left st in
     let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
     if len_right >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (n0, node_id_cnt1) =
         betree_node_apply_messages_back self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
       Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1) end
+        self.betree_internal_pivot n n0, node_id_cnt1)
     else
       Return (Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0)
-    end
-  else begin
+  else
     let* (n, node_id_cnt0) =
       betree_node_apply_messages_back self.betree_internal_right params
         node_id_cnt msgs_right st in
     Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0) end
+      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -994,7 +994,8 @@ let betree_be_tree_lookup_back
     self.betree_be_tree_node_id_cnt n)
 
 (** [betree_main::main] *)
-let main_fwd : result unit = Return ()
+let main_fwd : result unit =
+  Return ()
 
 (** Unit test for [betree_main::main] *)
 let _ = assert_norm (main_fwd = Return ())
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 201778df..7e44928c 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -41,7 +41,8 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   let* _ = u64_add counter 1 in Return counter
 
 (** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1
+let betree_fresh_node_id_back (counter : u64) : result u64 =
+  u64_add counter 1
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
@@ -161,11 +162,11 @@ let rec betree_list_partition_at_pivot_fwd
     let (i, x) = hd in
     if i >= pivot
     then Return (BetreeListNil, BetreeListCons (i, x) tl)
-    else begin
+    else
       let* p = betree_list_partition_at_pivot_fwd t tl pivot in
       let (ls0, ls1) = p in
       let l = ls0 in
-      Return (BetreeListCons (i, x) l, ls1) end
+      Return (BetreeListCons (i, x) l, ls1)
   | BetreeListNil -> Return (BetreeListNil, BetreeListNil)
   end
 
@@ -296,10 +297,10 @@ let rec betree_node_lookup_first_message_for_key_back
     let (i, m) = x in
     if i >= key
     then Return ret
-    else begin
+    else
       let* next_msgs0 =
         betree_node_lookup_first_message_for_key_back key next_msgs ret in
-      Return (BetreeListCons (i, m) next_msgs0) end
+      Return (BetreeListCons (i, m) next_msgs0)
   | BetreeListNil -> Return ret
   end
 
@@ -312,7 +313,7 @@ let rec betree_node_apply_upserts_fwd
   =
   let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
   if b
-  then begin
+  then
     let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
     let (_, m) = msg in
     begin match m with
@@ -322,13 +323,13 @@ let rec betree_node_apply_upserts_fwd
       let* v = betree_upsert_update_fwd prev s in
       let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in
       betree_node_apply_upserts_fwd msgs0 (Some v) key st
-    end end
-  else begin
+    end
+  else
     let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in
     let* _ =
       betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
         BetreeMessageInsert v) in
-    Return (st0, v) end
+    Return (st0, v)
 
 (** [betree_main::betree::Node::{5}::apply_upserts] *)
 let rec betree_node_apply_upserts_back
@@ -339,7 +340,7 @@ let rec betree_node_apply_upserts_back
   =
   let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
   if b
-  then begin
+  then
     let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
     let (_, m) = msg in
     begin match m with
@@ -349,13 +350,13 @@ let rec betree_node_apply_upserts_back
       let* v = betree_upsert_update_fwd prev s in
       let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in
       betree_node_apply_upserts_back msgs0 (Some v) key st st0
-    end end
-  else begin
+    end
+  else
     let* (_, v) = core_option_option_unwrap_fwd u64 prev st in
     let* msgs0 =
       betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
         BetreeMessageInsert v) in
-    Return (st0, msgs0) end
+    Return (st0, msgs0)
 
 (** [betree_main::betree::Node::{5}::lookup] *)
 let rec betree_node_lookup_fwd
@@ -372,13 +373,13 @@ let rec betree_node_lookup_fwd
     | BetreeListCons p l ->
       let (k, msg) = p in
       if k <> key
-      then begin
+      then
         let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0
           in
         let* _ =
           betree_node_lookup_first_message_for_key_back key msgs
             (BetreeListCons (k, msg) l) in
-        Return (st1, opt) end
+        Return (st1, opt)
       else
         begin match msg with
         | BetreeMessageInsert v ->
@@ -436,13 +437,13 @@ and betree_node_lookup_back
     | BetreeListCons p l ->
       let (k, msg) = p in
       if k <> key
-      then begin
+      then
         let* _ =
           betree_node_lookup_first_message_for_key_back key msgs
             (BetreeListCons (k, msg) l) in
         let* (st2, node0) =
           betree_internal_lookup_in_children_back node key st1 st0 in
-        Return (st2, BetreeNodeInternal node0) end
+        Return (st2, BetreeNodeInternal node0)
       else
         begin match msg with
         | BetreeMessageInsert v ->
@@ -503,16 +504,16 @@ and betree_internal_lookup_in_children_back
   (decreases (betree_internal_lookup_in_children_decreases self key st))
   =
   if key < self.betree_internal_pivot
-  then begin
+  then
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_left key st st0 in
     Return (st1, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right) end
-  else begin
+      self.betree_internal_pivot n self.betree_internal_right)
+  else
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_right key st st0 in
     Return (st1, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n) end
+      self.betree_internal_pivot self.betree_internal_left n)
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -541,9 +542,9 @@ let rec betree_node_lookup_mut_in_bindings_back
     let (i, i0) = hd in
     if i >= key
     then Return ret
-    else begin
+    else
       let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0) end
+      Return (BetreeListCons (i, i0) tl0)
   | BetreeListNil -> Return ret
   end
 
@@ -556,7 +557,7 @@ let betree_node_apply_to_leaf_fwd_back
   let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
   let* b = betree_list_head_has_key_fwd u64 bindings0 key in
   if b
-  then begin
+  then
     let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
     begin match new_msg with
     | BetreeMessageInsert v ->
@@ -574,7 +575,7 @@ let betree_node_apply_to_leaf_fwd_back
       let* bindings2 =
         betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
       betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end end
+    end
   else
     begin match new_msg with
     | BetreeMessageInsert v ->
@@ -615,11 +616,11 @@ let rec betree_node_filter_messages_for_key_fwd_back
   | BetreeListCons p l ->
     let (k, m) = p in
     if k = key
-    then begin
+    then
       let* msgs0 =
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) in
-      betree_node_filter_messages_for_key_fwd_back key msgs0 end
+      betree_node_filter_messages_for_key_fwd_back key msgs0
     else Return (BetreeListCons (k, m) l)
   | BetreeListNil -> Return BetreeListNil
   end
@@ -650,10 +651,10 @@ let rec betree_node_lookup_first_message_after_key_back
   | BetreeListCons p next_msgs ->
     let (k, m) = p in
     if k = key
-    then begin
+    then
       let* next_msgs0 =
         betree_node_lookup_first_message_after_key_back key next_msgs ret in
-      Return (BetreeListCons (k, m) next_msgs0) end
+      Return (BetreeListCons (k, m) next_msgs0)
     else Return ret
   | BetreeListNil -> Return ret
   end
@@ -712,11 +713,11 @@ let betree_node_apply_to_internal_fwd_back
         betree_node_lookup_first_message_for_key_back key msgs msgs3
       end
     end
-  else begin
+  else
     let* msgs1 =
       betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
         new_msg) in
-    betree_node_lookup_first_message_for_key_back key msgs msgs1 end
+    betree_node_lookup_first_message_for_key_back key msgs msgs1
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
 let rec betree_node_apply_messages_to_internal_fwd_back
@@ -750,7 +751,7 @@ let rec betree_node_apply_messages_fwd
       betree_node_apply_messages_to_internal_fwd_back content msgs in
     let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
     if num_msgs >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st1, content1) =
         betree_internal_flush_fwd node params node_id_cnt content0 st0 in
       let* (st2, (node0, _)) =
@@ -758,27 +759,27 @@ let rec betree_node_apply_messages_fwd
         in
       let* (st3, _) =
         betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
-      Return (st3, ()) end
-    else begin
+      Return (st3, ())
+    else
       let* (st1, _) =
         betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
-      Return (st1, ()) end
+      Return (st1, ())
   | BetreeNodeLeaf node ->
     let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
     let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
     let* len = betree_list_len_fwd (u64 & u64) content0 in
     let* i = u64_mul 2 params.betree_params_split_size in
     if len >= i
-    then begin
+    then
       let* (st1, _) =
         betree_leaf_split_fwd node content0 params node_id_cnt st0 in
       let* (st2, _) =
         betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
-      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 end
-    else begin
+      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
+    else
       let* (st1, _) =
         betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
-      Return (st1, ()) end
+      Return (st1, ())
   end
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
@@ -798,7 +799,7 @@ and betree_node_apply_messages_back'a
       betree_node_apply_messages_to_internal_fwd_back content msgs in
     let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
     if num_msgs >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st2, content1) =
         betree_internal_flush_fwd node params node_id_cnt content0 st1 in
       let* (st3, (node0, node_id_cnt0)) =
@@ -806,18 +807,18 @@ and betree_node_apply_messages_back'a
         in
       let* _ =
         betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) end
-    else begin
+      Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
+    else
       let* _ =
         betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, (BetreeNodeInternal node, node_id_cnt)) end
+      Return (st0, (BetreeNodeInternal node, node_id_cnt))
   | BetreeNodeLeaf node ->
     let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
     let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
     let* len = betree_list_len_fwd (u64 & u64) content0 in
     let* i = u64_mul 2 params.betree_params_split_size in
     if len >= i
-    then begin
+    then
       let* (st2, new_node) =
         betree_leaf_split_fwd node content0 params node_id_cnt st1 in
       let* (st3, _) =
@@ -826,11 +827,11 @@ and betree_node_apply_messages_back'a
         in
       let* (st4, node_id_cnt0) =
         betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
-      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) end
-    else begin
+      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+    else
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
       Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len),
-        node_id_cnt)) end
+        node_id_cnt))
   end
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
@@ -850,7 +851,7 @@ and betree_node_apply_messages_back1
       betree_node_apply_messages_to_internal_fwd_back content msgs in
     let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
     if num_msgs >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st2, content1) =
         betree_internal_flush_fwd node params node_id_cnt content0 st1 in
       let* (st3, (node0, _)) =
@@ -858,28 +859,28 @@ and betree_node_apply_messages_back1
         in
       let* _ =
         betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 end
-    else begin
+      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
+    else
       let* _ =
         betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, ()) end
+      Return (st0, ())
   | BetreeNodeLeaf node ->
     let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
     let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
     let* len = betree_list_len_fwd (u64 & u64) content0 in
     let* i = u64_mul 2 params.betree_params_split_size in
     if len >= i
-    then begin
+    then
       let* (st2, _) =
         betree_leaf_split_fwd node content0 params node_id_cnt st1 in
       let* (st3, _) =
         betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
       let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
         in
-      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 end
-    else begin
+      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
+    else
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, ()) end
+      Return (st0, ())
   end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
@@ -897,7 +898,7 @@ and betree_internal_flush_fwd
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
   if len_left >= params.betree_params_min_flush_size
-  then begin
+  then
     let* (st0, _) =
       betree_node_apply_messages_fwd self.betree_internal_left params
         node_id_cnt msgs_left st in
@@ -909,7 +910,7 @@ and betree_internal_flush_fwd
         node_id_cnt msgs_left st st1 in
     let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
     if len_right >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st3, _) =
         betree_node_apply_messages_fwd self.betree_internal_right params
           node_id_cnt0 msgs_right st2 in
@@ -919,9 +920,9 @@ and betree_internal_flush_fwd
       let* (st5, ()) =
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st2 st4 in
-      Return (st5, BetreeListNil) end
-    else Return (st2, msgs_right) end
-  else begin
+      Return (st5, BetreeListNil)
+    else Return (st2, msgs_right)
+  else
     let* (st0, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
         node_id_cnt msgs_right st in
@@ -931,7 +932,7 @@ and betree_internal_flush_fwd
     let* (st2, ()) =
       betree_node_apply_messages_back1 self.betree_internal_right params
         node_id_cnt msgs_right st st1 in
-    Return (st2, msgs_left) end
+    Return (st2, msgs_left)
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back'a
@@ -949,7 +950,7 @@ and betree_internal_flush_back'a
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
   if len_left >= params.betree_params_min_flush_size
-  then begin
+  then
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_left params
         node_id_cnt msgs_left st in
@@ -961,7 +962,7 @@ and betree_internal_flush_back'a
         node_id_cnt msgs_left st st2 in
     let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
     if len_right >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st4, _) =
         betree_node_apply_messages_fwd self.betree_internal_right params
           node_id_cnt0 msgs_right st3 in
@@ -972,12 +973,11 @@ and betree_internal_flush_back'a
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st3 st5 in
       Return (st0, (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1)) end
+        self.betree_internal_pivot n n0, node_id_cnt1))
     else
       Return (st0, (Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0))
-    end
-  else begin
+  else
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
         node_id_cnt msgs_right st in
@@ -989,7 +989,6 @@ and betree_internal_flush_back'a
         node_id_cnt msgs_right st st2 in
     Return (st0, (Mkbetree_internal_t self.betree_internal_id
       self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0))
-    end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back1
@@ -1007,7 +1006,7 @@ and betree_internal_flush_back1
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
   if len_left >= params.betree_params_min_flush_size
-  then begin
+  then
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_left params
         node_id_cnt msgs_left st in
@@ -1019,7 +1018,7 @@ and betree_internal_flush_back1
         node_id_cnt msgs_left st st2 in
     let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
     if len_right >= params.betree_params_min_flush_size
-    then begin
+    then
       let* (st4, _) =
         betree_node_apply_messages_fwd self.betree_internal_right params
           node_id_cnt0 msgs_right st3 in
@@ -1029,9 +1028,9 @@ and betree_internal_flush_back1
       let* _ =
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st3 st5 in
-      Return (st0, ()) end
-    else Return (st0, ()) end
-  else begin
+      Return (st0, ())
+    else Return (st0, ())
+  else
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
         node_id_cnt msgs_right st in
@@ -1041,7 +1040,7 @@ and betree_internal_flush_back1
     let* _ =
       betree_node_apply_messages_back1 self.betree_internal_right params
         node_id_cnt msgs_right st st2 in
-    Return (st0, ()) end
+    Return (st0, ())
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -1226,7 +1225,8 @@ let betree_be_tree_lookup_back
     self.betree_be_tree_node_id_cnt n)
 
 (** [betree_main::main] *)
-let main_fwd : result unit = Return ()
+let main_fwd : result unit =
+  Return ()
 
 (** Unit test for [betree_main::main] *)
 let _ = assert_norm (main_fwd = Return ())
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 0140aadc..62799976 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -8,7 +8,8 @@ include Hashmap.Clauses
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::hash_key] *)
-let hash_key_fwd (k : usize) : result usize = Return k
+let hash_key_fwd (k : usize) : result usize =
+  Return k
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 let rec hash_map_allocate_slots_loop_fwd
@@ -17,10 +18,10 @@ let rec hash_map_allocate_slots_loop_fwd
   (decreases (hash_map_allocate_slots_loop_decreases t slots n))
   =
   if n > 0
-  then begin
+  then
     let* slots0 = vec_push_back (list_t t) slots ListNil in
     let* n0 = usize_sub n 1 in
-    hash_map_allocate_slots_loop_fwd t slots0 n0 end
+    hash_map_allocate_slots_loop_fwd t slots0 n0
   else Return slots
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
@@ -52,10 +53,10 @@ let rec hash_map_clear_loop_fwd_back
   =
   let i0 = vec_len (list_t t) slots in
   if i < i0
-  then begin
+  then
     let* i1 = usize_add i 1 in
     let* slots0 = vec_index_mut_back (list_t t) slots i ListNil in
-    hash_map_clear_loop_fwd_back t slots0 i1 end
+    hash_map_clear_loop_fwd_back t slots0 i1
   else Return slots
 
 (** [hashmap::HashMap::{0}::clear] *)
@@ -98,9 +99,9 @@ let rec hash_map_insert_in_list_loop_back
   | ListCons ckey cvalue tl ->
     if ckey = key
     then Return (ListCons ckey value tl)
-    else begin
+    else
       let* tl0 = hash_map_insert_in_list_loop_back t key value tl in
-      Return (ListCons ckey cvalue tl0) end
+      Return (ListCons ckey cvalue tl0)
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
 
@@ -120,17 +121,17 @@ let hash_map_insert_no_resize_fwd_back
   let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in
   let* inserted = hash_map_insert_in_list_fwd t key value l in
   if inserted
-  then begin
+  then
     let* i0 = usize_add self.hash_map_num_entries 1 in
     let* l0 = hash_map_insert_in_list_back t key value l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
     Return (Mkhash_map_t i0 self.hash_map_max_load_factor
-      self.hash_map_max_load v) end
-  else begin
+      self.hash_map_max_load v)
+  else
     let* l0 = hash_map_insert_in_list_back t key value l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
     Return (Mkhash_map_t self.hash_map_num_entries
-      self.hash_map_max_load_factor self.hash_map_max_load v) end
+      self.hash_map_max_load_factor self.hash_map_max_load v)
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -162,14 +163,14 @@ let rec hash_map_move_elements_loop_fwd_back
   =
   let i0 = vec_len (list_t t) slots in
   if i < i0
-  then begin
+  then
     let* l = vec_index_mut_fwd (list_t t) slots i in
     let ls = mem_replace_fwd (list_t t) l ListNil in
     let* ntable0 = hash_map_move_elements_from_list_fwd_back t ntable ls in
     let* i1 = usize_add i 1 in
     let l0 = mem_replace_back (list_t t) l ListNil in
     let* slots0 = vec_index_mut_back (list_t t) slots i l0 in
-    hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end
+    hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
   else Return (ntable, slots)
 
 (** [hashmap::HashMap::{0}::move_elements] *)
@@ -188,13 +189,13 @@ let hash_map_try_resize_fwd_back
   let (i, i0) = self.hash_map_max_load_factor in
   let* i1 = usize_div n1 i in
   if capacity <= i1
-  then begin
+  then
     let* i2 = usize_mul capacity 2 in
     let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in
     let* (ntable0, _) =
       hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in
     Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
-      ntable0.hash_map_max_load ntable0.hash_map_slots) end
+      ntable0.hash_map_max_load ntable0.hash_map_slots)
   else
     Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
       self.hash_map_max_load self.hash_map_slots)
@@ -293,9 +294,9 @@ let rec hash_map_get_mut_in_list_loop_back
   | ListCons ckey cvalue tl ->
     if ckey = key
     then Return (ListCons ckey ret tl)
-    else begin
+    else
       let* tl0 = hash_map_get_mut_in_list_loop_back t tl key ret in
-      Return (ListCons ckey cvalue tl0) end
+      Return (ListCons ckey cvalue tl0)
   | ListNil -> Fail Failure
   end
 
@@ -366,9 +367,9 @@ let rec hash_map_remove_from_list_loop_back
       | ListCons i cvalue tl0 -> Return tl0
       | ListNil -> Fail Failure
       end
-    else begin
+    else
       let* tl0 = hash_map_remove_from_list_loop_back t key tl in
-      Return (ListCons ckey x tl0) end
+      Return (ListCons ckey x tl0)
   | ListNil -> Return ListNil
   end
 
@@ -423,31 +424,31 @@ let test1_fwd : result unit =
   let* i = hash_map_get_fwd u64 hm3 128 in
   if not (i = 18)
   then Fail Failure
-  else begin
+  else
     let* hm4 = hash_map_get_mut_back u64 hm3 1024 56 in
     let* i0 = hash_map_get_fwd u64 hm4 1024 in
     if not (i0 = 56)
     then Fail Failure
-    else begin
+    else
       let* x = hash_map_remove_fwd u64 hm4 1024 in
       begin match x with
       | None -> Fail Failure
       | Some x0 ->
         if not (x0 = 56)
         then Fail Failure
-        else begin
+        else
           let* hm5 = hash_map_remove_back u64 hm4 1024 in
           let* i1 = hash_map_get_fwd u64 hm5 0 in
           if not (i1 = 42)
           then Fail Failure
-          else begin
+          else
             let* i2 = hash_map_get_fwd u64 hm5 128 in
             if not (i2 = 18)
             then Fail Failure
-            else begin
+            else
               let* i3 = hash_map_get_fwd u64 hm5 1056 in
-              if not (i3 = 256) then Fail Failure else Return () end end end
-      end end end
+              if not (i3 = 256) then Fail Failure else Return ()
+      end
 
 (** Unit test for [hashmap::test1] *)
 let _ = assert_norm (test1_fwd = Return ())
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 51021daf..7e1a7636 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -9,7 +9,8 @@ include HashmapMain.Clauses
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap_main::hashmap::hash_key] *)
-let hashmap_hash_key_fwd (k : usize) : result usize = Return k
+let hashmap_hash_key_fwd (k : usize) : result usize =
+  Return k
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 let rec hashmap_hash_map_allocate_slots_loop_fwd
@@ -18,10 +19,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd
   (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n))
   =
   if n > 0
-  then begin
+  then
     let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in
     let* n0 = usize_sub n 1 in
-    hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end
+    hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
   else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
@@ -56,11 +57,11 @@ let rec hashmap_hash_map_clear_loop_fwd_back
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
-  then begin
+  then
     let* i1 = usize_add i 1 in
     let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
       in
-    hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end
+    hashmap_hash_map_clear_loop_fwd_back t slots0 i1
   else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
@@ -105,9 +106,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return (HashmapListCons ckey value tl)
-    else begin
+    else
       let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in
-      Return (HashmapListCons ckey cvalue tl0) end
+      Return (HashmapListCons ckey cvalue tl0)
   | HashmapListNil ->
     let l = HashmapListNil in Return (HashmapListCons key value l)
   end
@@ -132,22 +133,21 @@ let hashmap_hash_map_insert_no_resize_fwd_back
     in
   let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in
   if inserted
-  then begin
+  then
     let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in
     let* l0 = hashmap_hash_map_insert_in_list_back t key value l in
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
     Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
-      self.hashmap_hash_map_max_load v) end
-  else begin
+      self.hashmap_hash_map_max_load v)
+  else
     let* l0 = hashmap_hash_map_insert_in_list_back t key value l in
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
     Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
       self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
-    end
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -183,7 +183,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
-  then begin
+  then
     let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in
     let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
     let* ntable0 =
@@ -191,7 +191,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
     let* i1 = usize_add i 1 in
     let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
     let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in
-    hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end
+    hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
   else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
@@ -211,14 +211,14 @@ let hashmap_hash_map_try_resize_fwd_back
   let (i, i0) = self.hashmap_hash_map_max_load_factor in
   let* i1 = usize_div n1 i in
   if capacity <= i1
-  then begin
+  then
     let* i2 = usize_mul capacity 2 in
     let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in
     let* (ntable0, _) =
       hashmap_hash_map_move_elements_fwd_back t ntable
         self.hashmap_hash_map_slots 0 in
     Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
-      ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end
+      ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)
   else
     Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
       self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
@@ -321,9 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return (HashmapListCons ckey ret tl)
-    else begin
+    else
       let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in
-      Return (HashmapListCons ckey cvalue tl0) end
+      Return (HashmapListCons ckey cvalue tl0)
   | HashmapListNil -> Fail Failure
   end
 
@@ -406,9 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back
       | HashmapListCons i cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail Failure
       end
-    else begin
+    else
       let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in
-      Return (HashmapListCons ckey x tl0) end
+      Return (HashmapListCons ckey x tl0)
   | HashmapListNil -> Return HashmapListNil
   end
 
@@ -475,31 +475,31 @@ let hashmap_test1_fwd : result unit =
   let* i = hashmap_hash_map_get_fwd u64 hm3 128 in
   if not (i = 18)
   then Fail Failure
-  else begin
+  else
     let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in
     let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in
     if not (i0 = 56)
     then Fail Failure
-    else begin
+    else
       let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in
       begin match x with
       | None -> Fail Failure
       | Some x0 ->
         if not (x0 = 56)
         then Fail Failure
-        else begin
+        else
           let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in
           let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in
           if not (i1 = 42)
           then Fail Failure
-          else begin
+          else
             let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in
             if not (i2 = 18)
             then Fail Failure
-            else begin
+            else
               let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in
-              if not (i3 = 256) then Fail Failure else Return () end end end
-      end end end
+              if not (i3 = 256) then Fail Failure else Return ()
+      end
 
 (** Unit test for [hashmap_main::hashmap::test1] *)
 let _ = assert_norm (hashmap_test1_fwd = Return ())
@@ -513,7 +513,8 @@ let insert_on_disk_fwd
   Return (st1, ())
 
 (** [hashmap_main::main] *)
-let main_fwd : result unit = Return ()
+let main_fwd : result unit =
+  Return ()
 
 (** Unit test for [hashmap_main::main] *)
 let _ = assert_norm (main_fwd = Return ())
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
 
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 1b03b7a2..78ed970a 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -5,7 +5,8 @@ import Hashmap.Types
 import Hashmap.Clauses.Clauses
 
 /- [hashmap::hash_key] -/
-def hash_key_fwd (k : USize) : result USize := result.ret k
+def hash_key_fwd (k : USize) : result USize :=
+  result.ret k
 
 /- [hashmap::HashMap::{0}::allocate_slots] -/
 def hash_map_allocate_slots_loop_fwd
@@ -119,7 +120,8 @@ def hash_map_insert_in_list_loop_back
         let tl0 <- hash_map_insert_in_list_loop_back T key value tl
         result.ret (list_t.ListCons ckey cvalue tl0)
   | list_t.ListNil =>
-    let l := list_t.ListNil result.ret (list_t.ListCons key value l)
+    let l := list_t.ListNil
+    result.ret (list_t.ListCons key value l)
   
 termination_by hash_map_insert_in_list_loop_back key value ls =>
   hash_map_insert_in_list_loop_terminates T key value ls
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 2795ecfa..5b7d6f46 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -8,7 +8,8 @@ import HashmapMain.Clauses.Clauses
 section variable (opaque_defs: OpaqueDefs)
 
 /- [hashmap_main::hashmap::hash_key] -/
-def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k
+def hashmap_hash_key_fwd (k : USize) : result USize :=
+  result.ret k
 
 /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
 def hashmap_hash_map_allocate_slots_loop_fwd
@@ -638,7 +639,8 @@ def insert_on_disk_fwd
     result.ret (st1, ())
 
 /- [hashmap_main::main] -/
-def main_fwd : result Unit := result.ret ()
+def main_fwd : result Unit :=
+  result.ret ()
 
 /- Unit test for [hashmap_main::main] -/
 #assert (main_fwd = .ret ())
diff --git a/tests/lean/misc/constants/Constants.lean b/tests/lean/misc/constants/Constants.lean
index a5cbe363..9ef9ca44 100644
--- a/tests/lean/misc/constants/Constants.lean
+++ b/tests/lean/misc/constants/Constants.lean
@@ -82,7 +82,8 @@ structure OpaqueDefs where
   def y_c : wrap_t Int32 := eval_global y_body (by simp)
   
   /- [constants::unwrap_y] -/
-  def unwrap_y_fwd : result Int32 := result.ret y_c.wrap_val
+  def unwrap_y_fwd : result Int32 :=
+    result.ret y_c.wrap_val
   
   /- [constants::YVAL] -/
   def yval_body : result Int32 := unwrap_y_fwd
@@ -94,10 +95,12 @@ structure OpaqueDefs where
   def get_z1_z1_c : Int32 := eval_global get_z1_z1_body (by simp)
   
   /- [constants::get_z1] -/
-  def get_z1_fwd : result Int32 := result.ret get_z1_z1_c
+  def get_z1_fwd : result Int32 :=
+    result.ret get_z1_z1_c
   
   /- [constants::add] -/
-  def add_fwd (a : Int32) (b : Int32) : result Int32 := Int32.checked_add a b
+  def add_fwd (a : Int32) (b : Int32) : result Int32 :=
+    Int32.checked_add a b
   
   /- [constants::Q1] -/
   def q1_body : result Int32 := result.ret (Int32.ofNatCore 5 (by intlit))
diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean
index 33a3a881..8b7e8a1f 100644
--- a/tests/lean/misc/loops/Loops/Funs.lean
+++ b/tests/lean/misc/loops/Loops/Funs.lean
@@ -221,7 +221,8 @@ def get_elem_shared_fwd
     get_elem_shared_loop_fwd x l
 
 /- [loops::id_mut] -/
-def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := result.ret ls
+def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) :=
+  result.ret ls
 
 /- [loops::id_mut] -/
 def id_mut_back
diff --git a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
index d871392b..53093519 100644
--- a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
@@ -30,7 +30,8 @@ structure OpaqueDefs where
   | SumRight : T2 -> sum_t T1 T2
   
   /- [no_nested_borrows::neg_test] -/
-  def neg_test_fwd (x : Int32) : result Int32 := Int32.checked_neg x
+  def neg_test_fwd (x : Int32) : result Int32 :=
+    Int32.checked_neg x
   
   /- [no_nested_borrows::add_test] -/
   def add_test_fwd (x : UInt32) (y : UInt32) : result UInt32 :=
@@ -53,7 +54,8 @@ structure OpaqueDefs where
     UInt32.checked_rem x y
   
   /- [no_nested_borrows::cast_test] -/
-  def cast_test_fwd (x : UInt32) : result Int32 := scalar_cast Int32 x
+  def cast_test_fwd (x : UInt32) : result Int32 :=
+    scalar_cast Int32 x
   
   /- [no_nested_borrows::test2] -/
   def test2_fwd : result Unit :=
@@ -128,7 +130,8 @@ structure OpaqueDefs where
   #assert (refs_test2_fwd = .ret ())
   
   /- [no_nested_borrows::test_list1] -/
-  def test_list1_fwd : result Unit := result.ret ()
+  def test_list1_fwd : result Unit :=
+    result.ret ()
   
   /- Unit test for [no_nested_borrows::test_list1] -/
   #assert (test_list1_fwd = .ret ())
@@ -145,7 +148,8 @@ structure OpaqueDefs where
   #assert (test_box1_fwd = .ret ())
   
   /- [no_nested_borrows::copy_int] -/
-  def copy_int_fwd (x : Int32) : result Int32 := result.ret x
+  def copy_int_fwd (x : Int32) : result Int32 :=
+    result.ret x
   
   /- [no_nested_borrows::test_unreachable] -/
   def test_unreachable_fwd (b : Bool) : result Unit :=
@@ -240,7 +244,8 @@ structure OpaqueDefs where
   #assert (choose_test_fwd = .ret ())
   
   /- [no_nested_borrows::test_char] -/
-  def test_char_fwd : result Char := result.ret 'a'
+  def test_char_fwd : result Char :=
+    result.ret 'a'
   
   /- [no_nested_borrows::NodeElem] -/
   mutual inductive node_elem_t (T : Type) :=
@@ -389,16 +394,19 @@ structure OpaqueDefs where
   /- [no_nested_borrows::id_mut_pair1] -/
   def id_mut_pair1_back
     (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := ret0 result.ret (t, t0)
+    let (t, t0) := ret0
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair2] -/
   def id_mut_pair2_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := p result.ret (t, t0)
+    let (t, t0) := p
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair2] -/
   def id_mut_pair2_back
     (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := ret0 result.ret (t, t0)
+    let (t, t0) := ret0
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair3] -/
   def id_mut_pair3_fwd (T1 T2 : Type) (x : T1) (y : T2) : result (T1 × T2) :=
@@ -416,7 +424,8 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::id_mut_pair4] -/
   def id_mut_pair4_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := p result.ret (t, t0)
+    let (t, t0) := p
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair4] -/
   def id_mut_pair4_back'a
@@ -505,7 +514,8 @@ structure OpaqueDefs where
   #assert (test_constants_fwd = .ret ())
   
   /- [no_nested_borrows::test_weird_borrows1] -/
-  def test_weird_borrows1_fwd : result Unit := result.ret ()
+  def test_weird_borrows1_fwd : result Unit :=
+    result.ret ()
   
   /- Unit test for [no_nested_borrows::test_weird_borrows1] -/
   #assert (test_weird_borrows1_fwd = .ret ())