1 files changed, 28 insertions, 27 deletions

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 ())