verusfmt

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

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 ---------------- //

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

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

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;

source/vstd/std_specs/range.rs

@@ -197,4 +197,4 @@ pub broadcast group range_axioms {
     axiom_spec_range_next_isize,
 }
 
-} // verus!
+} // verus!

source/vstd/vstd.rs

@@ -75,4 +75,4 @@ pub broadcast group vstd_axioms {
     std_specs::range::range_axioms,
 }
 
-} // verus!
+} // verus!