Diagnose weird indenting issue with call to assert_seqs_equal as inte…

…nded

behavior due to macro call

examples/wip.rs

@@ -1,17 +1,15 @@
 verus! {
 
-// Why the extra newline for the semi-colon?
-// Answer: The parser sees the `;` as redundant and treats it as a separate statement
-fn test() -> u64 {
-    proof { assert_sets_equal!(a, b); };
-    proof {
-        assert_sets_equal!(a, b);
-        assert_sets_equal!(c, d);
-    };
-    5
-
+// Weird indenting of the last line
+// Answer: This is because we don't format inside macro calls
+proof fn test() {
+    assert_seqs_equal!(v@,
+                   old(v)@.subrange(0, start as int) +
+                   old(v)@.subrange(start as int + deleted as int,
+                                               old(v)@.len() as int));
 }
 
+
 /*
 // The first set of &&& get out-dented, while the second one is absorbed into a single line
 fn clone_value() -> (out: u8)
@@ -28,13 +26,5 @@ fn clone_value() -> (out: u8)
 {
 }
 
-// Weird indenting of the last line
-proof fn test() {
-    assert_seqs_equal!(v@,
-                   old(v)@.subrange(0, start as int) +
-                   old(v)@.subrange(start as int + deleted as int,
-                                               old(v)@.len() as int));
-}
-
 */
 } // verus!