Improve formatting further by removing useless spaces

2 files changed, 0 insertions, 28 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 ())