When using matches, or ('||') is parsed as closure ('| |').

[JoPolzin]

When running verusfmt on the following code:

proof fn foo() {
    assert(a matches b || true)
}

it becomes this:

proof fn foo() {
    assert(a matches b |  | true)
}

I strongly suspect, this is because they are being interpretated as closures, instead of or`s.
Also, i only encounterd this problem, when using matches, so far.

[jaybosamiya-ms]

Thanks for the report!

The diff that fixes this (and doesn't seem to break any of our test cases)

diff --git a/src/verus.pest b/src/verus.pest
index 04223d9..cd2a8bb 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -1553,7 +1553,7 @@ pat = {
         // range_pat (for 1.. or 1..2)
         (dot_dot_eq_str | dot_dot_str) ~ pat?
         // or_pat
-      | (pipe_str ~ pat_inner)* ~ pipe_str?
+      | (pipe_str ~ pat_inner)*
     )?
 }

I don't really know why that particular thing exists in the pattern grammar though. None of our test cases seemingly need it, and I can't even think of how the extra pipe_str? thing there makes sense. Turns out it originates from the very first commit that introduces the grammar (which had a "|"? instead, but essentially same thing).

If you'd like to package up the above diff, along with a test case (in tests/verus_consistency.rs) that acts as a regression test for this issue, and make a PR for it, that'd be great!