Failed to parse !~=

[bbayazit16]

verusfmt can't format this document:

use vstd::prelude::*;

verus! {
    proof fn my_proof() {
        let a = Seq::empty().push(4int);
        let b = Seq::empty().push(0int);

        assert(a[0] !~= b[0]);
    }
}

fn main() {}

$ verusfmt src/main.rs:

Error: 
  × Failed to parse
   ╭─[src/main.rs:8:22]
 7 │ 
 8 │         assert(a[0] !~= b[0]);
   ·                      ┬
   ·                      ╰── here
 9 │     }
   ╰────
  help: Expected one of: COMMENT, has_str, is_str

whereas Verus verification passes, and Verus analyzer doesn't complain.

$ verusfmt --version:
verusfmt 0.5.6

[parno]

We do want to ensure that verusfmt and verus behave consistently, but can I ask about the context where you're using !~=? In general, we wouldn't expect that to give results that differ significantly from !=, so we might remove Verus's support for !~=. For example, your sample code verifies with just assert(a[0] != b[0]);

[bbayazit16]

In my case, replacing !~= with != works. I was using !~= because I thought it was more natural for those reading the code (if =~= is extensional equality, then !~= should be 'not extensionally equal').

[parno]

Okay, thanks for confirming. I think it's the case that if you assert a != b, then Verus should be able to prove that by considering the respective lengths and individual elements; i.e., you don't need to explicitly invoke extensional equality. In the other direction, a == b, Verus doesn't always consider extensional equality of its own volition, which is why we need the extra operator.