diff --git a/source/vstd/map.rs b/source/vstd/map.rs
index 671b137375..0bec6177d5 100644
--- a/source/vstd/map.rs
+++ b/source/vstd/map.rs
@@ -308,7 +308,7 @@ pub broadcast group map_axioms {
     axiom_map_remove_domain,
     axiom_map_remove_different,
     axiom_map_ext_equal,
-    axiom_map_ext_equal_deep, 
+    axiom_map_ext_equal_deep,
 }
 
 // Macros
diff --git a/source/vstd/seq.rs b/source/vstd/seq.rs
index aa0f94d2c7..eaf2d9a666 100644
--- a/source/vstd/seq.rs
+++ b/source/vstd/seq.rs
@@ -351,7 +351,7 @@ pub broadcast group seq_axioms {
     axiom_seq_subrange_index,
     axiom_seq_add_len,
     axiom_seq_add_index1,
-    axiom_seq_add_index2 
+    axiom_seq_add_index2,
 }
 
 // ------------- Macros ---------------- //
diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs
index 9110da3b2b..b1f238e018 100644
--- a/source/vstd/seq_lib.rs
+++ b/source/vstd/seq_lib.rs
@@ -16,7 +16,7 @@ use builtin::*;
 use builtin_macros::*;
 
 verus! {
-    
+
 broadcast use seq_axioms;
 
 impl<A> Seq<A> {
@@ -1000,7 +1000,7 @@ impl<A> Seq<Seq<A>> {
         decreases self.len(),
     {
         broadcast use seq_lib_default;
-        admit(); // TODO
+        admit();  // TODO
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
             seq![self.last()].lemma_flatten_one_element();
diff --git a/source/vstd/set_lib.rs b/source/vstd/set_lib.rs
index 0484e121a7..9e77ed2068 100644
--- a/source/vstd/set_lib.rs
+++ b/source/vstd/set_lib.rs
@@ -13,7 +13,7 @@ use builtin::*;
 use builtin_macros::*;
 
 verus! {
-    
+
 broadcast use crate::set::set_axioms;
 
 impl<A> Set<A> {
@@ -855,7 +855,7 @@ pub broadcast proof fn axiom_is_empty<A>(s: Set<A>)
     ensures
         exists|a: A| s.contains(a),
 {
-    admit(); // REVIEW, should this be in `set`, or have a proof?
+    admit();  // REVIEW, should this be in `set`, or have a proof?
 }
 
 #[doc(hidden)]
diff --git a/source/vstd/std_specs/bits.rs b/source/vstd/std_specs/bits.rs
index 43b647c8fe..9506fb78a1 100644
--- a/source/vstd/std_specs/bits.rs
+++ b/source/vstd/std_specs/bits.rs
@@ -707,7 +707,7 @@ pub broadcast proof fn axiom_u64_leading_zeros(i: u64)
         forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 0u64,
     decreases i,
 {
-    admit(); // TODO
+    admit();  // TODO
     // assert(i / 2 == (i >> 1u64)) by (bit_vector);
     // assert(((i >> 1) >> sub(63u64, 0)) & 1u64 == 0u64) by (bit_vector);
     // let x = u64_leading_zeros(i / 2) as u64;
diff --git a/source/vstd/std_specs/range.rs b/source/vstd/std_specs/range.rs
index f615091141..9e79551c81 100644
--- a/source/vstd/std_specs/range.rs
+++ b/source/vstd/std_specs/range.rs
@@ -197,4 +197,4 @@ pub broadcast group range_axioms {
     axiom_spec_range_next_isize,
 }
 
-} // verus!
\ No newline at end of file
+} // verus!
diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs
index d3baaadb26..092d782317 100644
--- a/source/vstd/vstd.rs
+++ b/source/vstd/vstd.rs
@@ -75,4 +75,4 @@ pub broadcast group vstd_axioms {
     std_specs::range::range_axioms,
 }
 
-} // verus!
\ No newline at end of file
+} // verus!