Improve formatting further by removing useless spaces

5 files changed, 33 insertions, 90 deletions

diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 78ed970a..3bdd9dd2 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -98,7 +98,6 @@ def hash_map_insert_in_list_loop_fwd
     then result.ret false
     else hash_map_insert_in_list_loop_fwd T key value tl
   | list_t.ListNil => result.ret true
-  
 termination_by hash_map_insert_in_list_loop_fwd key value ls =>
   hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
@@ -122,7 +121,6 @@ def hash_map_insert_in_list_loop_back
   | list_t.ListNil =>
     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
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
@@ -185,7 +183,6 @@ def hash_map_move_elements_from_list_loop_fwd_back
       let ntable0 <- hash_map_insert_no_resize_fwd_back T ntable k v
       hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
   | list_t.ListNil => result.ret ntable
-  
 termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls =>
   hash_map_move_elements_from_list_loop_terminates T ntable ls
 decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls
@@ -277,7 +274,6 @@ def hash_map_contains_key_in_list_loop_fwd
     then result.ret true
     else hash_map_contains_key_in_list_loop_fwd T key tl
   | list_t.ListNil => result.ret false
-  
 termination_by hash_map_contains_key_in_list_loop_fwd key ls =>
   hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hash_map_contains_key_in_list_loop_decreases key ls
@@ -306,7 +302,6 @@ def hash_map_get_in_list_loop_fwd
     then result.ret cvalue
     else hash_map_get_in_list_loop_fwd T key tl
   | list_t.ListNil => result.fail error.panic
-  
 termination_by hash_map_get_in_list_loop_fwd key ls =>
   hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hash_map_get_in_list_loop_decreases key ls
@@ -335,7 +330,6 @@ def hash_map_get_mut_in_list_loop_fwd
     then result.ret cvalue
     else hash_map_get_mut_in_list_loop_fwd T tl key
   | list_t.ListNil => result.fail error.panic
-  
 termination_by hash_map_get_mut_in_list_loop_fwd ls key =>
   hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
@@ -357,7 +351,6 @@ def hash_map_get_mut_in_list_loop_back
         let tl0 <- hash_map_get_mut_in_list_loop_back T tl key ret0
         result.ret (list_t.ListCons ckey cvalue tl0)
   | list_t.ListNil => result.fail error.panic
-  
 termination_by hash_map_get_mut_in_list_loop_back ls key ret0 =>
   hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
@@ -409,10 +402,8 @@ def hash_map_remove_from_list_loop_fwd
       match mv_ls with
       | list_t.ListCons i cvalue tl0 => result.ret (Option.some cvalue)
       | list_t.ListNil => result.fail error.panic
-      
     else hash_map_remove_from_list_loop_fwd T key tl
   | list_t.ListNil => result.ret Option.none
-  
 termination_by hash_map_remove_from_list_loop_fwd key ls =>
   hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
@@ -434,13 +425,11 @@ def hash_map_remove_from_list_loop_back
       match mv_ls with
       | list_t.ListCons i cvalue tl0 => result.ret tl0
       | list_t.ListNil => result.fail error.panic
-      
     else
       do
         let tl0 <- hash_map_remove_from_list_loop_back T key tl
         result.ret (list_t.ListCons ckey t tl0)
   | list_t.ListNil => result.ret list_t.ListNil
-  
 termination_by hash_map_remove_from_list_loop_back key ls =>
   hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
@@ -466,7 +455,6 @@ def hash_map_remove_fwd
         let _ <- USize.checked_sub self.hash_map_num_entries
           (USize.ofNatCore 1 (by intlit))
         result.ret (Option.some x0)
-    
 
 /- [hashmap::HashMap::{0}::remove] -/
 def hash_map_remove_back
@@ -502,7 +490,6 @@ def hash_map_remove_back
             hash_map_max_load := self.hash_map_max_load,
             hash_map_slots := v
           }
-    
 
 /- [hashmap::test1] -/
 def test1_fwd : result Unit :=
@@ -565,7 +552,6 @@ def test1_fwd : result Unit :=
                           if not (i3 = (UInt64.ofNatCore 256 (by intlit)))
                           then result.fail error.panic
                           else result.ret ()
-            
 
 /- Unit test for [hashmap::test1] -/
 #assert (test1_fwd = .ret ())
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 5b7d6f46..1abc9f8d 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -110,7 +110,6 @@ def hashmap_hash_map_insert_in_list_loop_fwd
     then result.ret false
     else hashmap_hash_map_insert_in_list_loop_fwd T key value tl
   | hashmap_list_t.HashmapListNil => result.ret true
-  
 termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls =>
   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
@@ -136,7 +135,6 @@ def hashmap_hash_map_insert_in_list_loop_back
   | hashmap_list_t.HashmapListNil =>
     let l := hashmap_list_t.HashmapListNil
     result.ret (hashmap_list_t.HashmapListCons key value l)
-  
 termination_by hashmap_hash_map_insert_in_list_loop_back key value ls =>
   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
@@ -206,7 +204,6 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back
       let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v
       hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
   | hashmap_list_t.HashmapListNil => result.ret ntable
-  
 termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
   =>
   hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls
@@ -306,7 +303,6 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd
     then result.ret true
     else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl
   | hashmap_list_t.HashmapListNil => result.ret false
-  
 termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls =>
   hashmap_hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls
@@ -336,7 +332,6 @@ def hashmap_hash_map_get_in_list_loop_fwd
     then result.ret cvalue
     else hashmap_hash_map_get_in_list_loop_fwd T key tl
   | hashmap_list_t.HashmapListNil => result.fail error.panic
-  
 termination_by hashmap_hash_map_get_in_list_loop_fwd key ls =>
   hashmap_hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls
@@ -366,7 +361,6 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd
     then result.ret cvalue
     else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key
   | hashmap_list_t.HashmapListNil => result.fail error.panic
-  
 termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key =>
   hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
@@ -390,7 +384,6 @@ def hashmap_hash_map_get_mut_in_list_loop_back
         let tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0
         result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0)
   | hashmap_list_t.HashmapListNil => result.fail error.panic
-  
 termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 =>
   hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
@@ -450,10 +443,8 @@ def hashmap_hash_map_remove_from_list_loop_fwd
       | hashmap_list_t.HashmapListCons i cvalue tl0 =>
         result.ret (Option.some cvalue)
       | hashmap_list_t.HashmapListNil => result.fail error.panic
-      
     else hashmap_hash_map_remove_from_list_loop_fwd T key tl
   | hashmap_list_t.HashmapListNil => result.ret Option.none
-  
 termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls =>
   hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
@@ -478,13 +469,11 @@ def hashmap_hash_map_remove_from_list_loop_back
       match mv_ls with
       | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0
       | hashmap_list_t.HashmapListNil => result.fail error.panic
-      
     else
       do
         let tl0 <- hashmap_hash_map_remove_from_list_loop_back T key tl
         result.ret (hashmap_list_t.HashmapListCons ckey t tl0)
   | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil
-  
 termination_by hashmap_hash_map_remove_from_list_loop_back key ls =>
   hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
@@ -513,7 +502,6 @@ def hashmap_hash_map_remove_fwd
         let _ <- USize.checked_sub self.hashmap_hash_map_num_entries
           (USize.ofNatCore 1 (by intlit))
         result.ret (Option.some x0)
-    
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove] -/
 def hashmap_hash_map_remove_back
@@ -556,7 +544,6 @@ def hashmap_hash_map_remove_back
             hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
             hashmap_hash_map_slots := v
           }
-    
 
 /- [hashmap_main::hashmap::test1] -/
 def hashmap_test1_fwd : result Unit :=
@@ -624,7 +611,6 @@ def hashmap_test1_fwd : result Unit :=
                           if not (i3 = (UInt64.ofNatCore 256 (by intlit)))
                           then result.fail error.panic
                           else result.ret ()
-            
 
 /- Unit test for [hashmap_main::hashmap::test1] -/
 #assert (hashmap_test1_fwd = .ret ())
diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean
index 8b7e8a1f..55f0c87d 100644
--- a/tests/lean/misc/loops/Loops/Funs.lean
+++ b/tests/lean/misc/loops/Loops/Funs.lean
@@ -80,9 +80,10 @@ def clear_fwd_back (v : vec UInt32) : result (vec UInt32) :=
 def list_mem_loop_fwd (x : UInt32) (ls : list_t UInt32) : (result Bool) :=
   match ls with
   | list_t.ListCons y tl =>
-    if y = x then result.ret true else list_mem_loop_fwd x tl
+    if y = x
+    then result.ret true
+    else list_mem_loop_fwd x tl
   | list_t.ListNil => result.ret false
-  
 termination_by list_mem_loop_fwd x ls => list_mem_loop_terminates x ls
 decreasing_by list_mem_loop_decreases x ls
 
@@ -102,7 +103,6 @@ def list_nth_mut_loop_loop_fwd
         let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_loop_fwd T tl i0
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_loop_fwd ls i =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -124,7 +124,6 @@ def list_nth_mut_loop_loop_back
         let tl0 <- list_nth_mut_loop_loop_back T tl i0 ret0
         result.ret (list_t.ListCons x tl0)
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_loop_back ls i ret0 =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -146,7 +145,6 @@ def list_nth_shared_loop_loop_fwd
         let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_loop_fwd T tl i0
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_loop_loop_fwd ls i =>
   list_nth_shared_loop_loop_terminates T ls i
 decreasing_by list_nth_shared_loop_loop_decreases ls i
@@ -160,9 +158,10 @@ def list_nth_shared_loop_fwd
 def get_elem_mut_loop_fwd (x : USize) (ls : list_t USize) : (result USize) :=
   match ls with
   | list_t.ListCons y tl =>
-    if y = x then result.ret y else get_elem_mut_loop_fwd x tl
+    if y = x
+    then result.ret y
+    else get_elem_mut_loop_fwd x tl
   | list_t.ListNil => result.fail error.panic
-  
 termination_by get_elem_mut_loop_fwd x ls => get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
 
@@ -185,7 +184,6 @@ def get_elem_mut_loop_back
         let tl0 <- get_elem_mut_loop_back x tl ret0
         result.ret (list_t.ListCons y tl0)
   | list_t.ListNil => result.fail error.panic
-  
 termination_by get_elem_mut_loop_back x ls ret0 =>
   get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
@@ -206,9 +204,10 @@ def get_elem_shared_loop_fwd
   (x : USize) (ls : list_t USize) : (result USize) :=
   match ls with
   | list_t.ListCons y tl =>
-    if y = x then result.ret y else get_elem_shared_loop_fwd x tl
+    if y = x
+    then result.ret y
+    else get_elem_shared_loop_fwd x tl
   | list_t.ListNil => result.fail error.panic
-  
 termination_by get_elem_shared_loop_fwd x ls =>
   get_elem_shared_loop_terminates x ls
 decreasing_by get_elem_shared_loop_decreases x ls
@@ -245,7 +244,6 @@ def list_nth_mut_loop_with_id_loop_fwd
         let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_with_id_loop_fwd T i0 tl
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_with_id_loop_fwd i ls =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -270,7 +268,6 @@ def list_nth_mut_loop_with_id_loop_back
         let tl0 <- list_nth_mut_loop_with_id_loop_back T i0 tl ret0
         result.ret (list_t.ListCons x tl0)
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -295,7 +292,6 @@ def list_nth_shared_loop_with_id_loop_fwd
         let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_with_id_loop_fwd T i0 tl
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_loop_with_id_loop_fwd i ls =>
   list_nth_shared_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls
@@ -323,9 +319,7 @@ def list_nth_mut_loop_pair_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -354,9 +348,7 @@ def list_nth_mut_loop_pair_loop_back'a
           let tl00 <- list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x0 tl00)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -385,9 +377,7 @@ def list_nth_mut_loop_pair_loop_back'b
           let tl10 <- list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x1 tl10)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -415,9 +405,7 @@ def list_nth_shared_loop_pair_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -445,9 +433,7 @@ def list_nth_mut_loop_pair_merge_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -479,9 +465,7 @@ def list_nth_mut_loop_pair_merge_loop_back
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x0 tl00, list_t.ListCons x1 tl10)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -509,9 +493,7 @@ def list_nth_shared_loop_pair_merge_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -539,9 +521,7 @@ def list_nth_mut_shared_loop_pair_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -570,9 +550,7 @@ def list_nth_mut_shared_loop_pair_loop_back
           let tl00 <- list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x0 tl00)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -600,9 +578,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -632,9 +608,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_back
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x0 tl00)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -662,9 +636,7 @@ def list_nth_shared_mut_loop_pair_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -693,9 +665,7 @@ def list_nth_shared_mut_loop_pair_loop_back
           let tl10 <- list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x1 tl10)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -723,9 +693,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -755,9 +723,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_back
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           result.ret (list_t.ListCons x1 tl10)
     | list_t.ListNil => result.fail error.panic
-    
   | list_t.ListNil => result.fail error.panic
-  
 termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
diff --git a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
index 53093519..608aabc1 100644
--- a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
@@ -69,7 +69,9 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::get_max] -/
   def get_max_fwd (x : UInt32) (y : UInt32) : result UInt32 :=
-    if x >= y then result.ret x else result.ret y
+    if x >= y
+    then result.ret x
+    else result.ret y
   
   /- [no_nested_borrows::test3] -/
   def test3_fwd : result Unit :=
@@ -153,11 +155,15 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::test_unreachable] -/
   def test_unreachable_fwd (b : Bool) : result Unit :=
-    if b then result.fail error.panic else result.ret ()
+    if b
+    then result.fail error.panic
+    else result.ret ()
   
   /- [no_nested_borrows::test_panic] -/
   def test_panic_fwd (b : Bool) : result Unit :=
-    if b then result.fail error.panic else result.ret ()
+    if b
+    then result.fail error.panic
+    else result.ret ()
   
   /- [no_nested_borrows::test_copy_int] -/
   def test_copy_int_fwd : result Unit :=
@@ -175,7 +181,6 @@ structure OpaqueDefs where
     match l with
     | list_t.ListCons t l0 => result.ret true
     | list_t.ListNil => result.ret false
-    
   
   /- [no_nested_borrows::test_is_cons] -/
   def test_is_cons_fwd : result Unit :=
@@ -183,7 +188,9 @@ structure OpaqueDefs where
       let l := list_t.ListNil
       let b <-
         is_cons_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) l)
-      if not b then result.fail error.panic else result.ret ()
+      if not b
+      then result.fail error.panic
+      else result.ret ()
   
   /- Unit test for [no_nested_borrows::test_is_cons] -/
   #assert (test_is_cons_fwd = .ret ())
@@ -193,7 +200,6 @@ structure OpaqueDefs where
     match l with
     | list_t.ListCons hd tl => result.ret (hd, tl)
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [no_nested_borrows::test_split_list] -/
   def test_split_list_fwd : result Unit :=
@@ -212,12 +218,16 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::choose] -/
   def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : result T :=
-    if b then result.ret x else result.ret y
+    if b
+    then result.ret x
+    else result.ret y
   
   /- [no_nested_borrows::choose] -/
   def choose_back
     (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : result (T × T) :=
-    if b then result.ret (ret0, y) else result.ret (x, ret0)
+    if b
+    then result.ret (ret0, y)
+    else result.ret (x, ret0)
   
   /- [no_nested_borrows::choose_test] -/
   def choose_test_fwd : result Unit :=
@@ -265,7 +275,6 @@ structure OpaqueDefs where
         let i <- list_length_fwd T l1
         UInt32.checked_add (UInt32.ofNatCore 1 (by intlit)) i
     | list_t.ListNil => result.ret (UInt32.ofNatCore 0 (by intlit))
-    
   
   /- [no_nested_borrows::list_nth_shared] -/
   def list_nth_shared_fwd (T : Type) (l : list_t T) (i : UInt32) : result T :=
@@ -278,7 +287,6 @@ structure OpaqueDefs where
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_fwd T tl i0
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : result T :=
@@ -291,7 +299,6 @@ structure OpaqueDefs where
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_back
@@ -306,7 +313,6 @@ structure OpaqueDefs where
           let tl0 <- list_nth_mut_back T tl i0 ret0
           result.ret (list_t.ListCons x tl0)
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [no_nested_borrows::list_rev_aux] -/
   def list_rev_aux_fwd
@@ -314,7 +320,6 @@ structure OpaqueDefs where
     match li with
     | list_t.ListCons hd tl => list_rev_aux_fwd T tl (list_t.ListCons hd lo)
     | list_t.ListNil => result.ret lo
-    
   
   /- [no_nested_borrows::list_rev] -/
   def list_rev_fwd_back (T : Type) (l : list_t T) : result (list_t T) :=
@@ -542,7 +547,6 @@ structure OpaqueDefs where
     match l with
     | list_t.ListCons i l0 => result.ret (UInt32.ofNatCore 1 (by intlit))
     | list_t.ListNil => result.ret (UInt32.ofNatCore 0 (by intlit))
-    
   
   /- [no_nested_borrows::test_shared_borrow_enum2] -/
   def test_shared_borrow_enum2_fwd : result UInt32 :=
diff --git a/tests/lean/misc/paper/Paper.lean b/tests/lean/misc/paper/Paper.lean
index 2d23f394..adcd1eae 100644
--- a/tests/lean/misc/paper/Paper.lean
+++ b/tests/lean/misc/paper/Paper.lean
@@ -21,12 +21,16 @@ structure OpaqueDefs where
   
   /- [paper::choose] -/
   def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : result T :=
-    if b then result.ret x else result.ret y
+    if b
+    then result.ret x
+    else result.ret y
   
   /- [paper::choose] -/
   def choose_back
     (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : result (T × T) :=
-    if b then result.ret (ret0, y) else result.ret (x, ret0)
+    if b
+    then result.ret (ret0, y)
+    else result.ret (x, ret0)
   
   /- [paper::test_choose] -/
   def test_choose_fwd : result Unit :=
@@ -68,7 +72,6 @@ structure OpaqueDefs where
           let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [paper::list_nth_mut] -/
   def list_nth_mut_back
@@ -83,7 +86,6 @@ structure OpaqueDefs where
           let tl0 <- list_nth_mut_back T tl i0 ret0
           result.ret (list_t.ListCons x tl0)
     | list_t.ListNil => result.fail error.panic
-    
   
   /- [paper::sum] -/
   def sum_fwd (l : list_t Int32) : result Int32 :=
@@ -92,7 +94,6 @@ structure OpaqueDefs where
                                 let i <- sum_fwd tl
                                 Int32.checked_add x i
     | list_t.ListNil => result.ret (Int32.ofNatCore 0 (by intlit))
-    
   
   /- [paper::test_nth] -/
   def test_nth_fwd : result Unit :=