Spec equality (==)

Verus/Rust difference

In spec mode, == is mathematical equality — it is not the same as == in exec code, which dispatches to the PartialEq trait.

For an introduction, see Equality.

Syntax

equality_expr ::= spec_expr == spec_expr
                | spec_expr != spec_expr

Typing

The expression is well-typed if both the left-hand side and right-hand side have the same type.

In some cases, Verus may also accept == as well-typed when both sides have the same mathematical interpretation. For example:

• Two integer types can always be compared.
• T can be compared to &T.

Semantics

The == operator returns true iff the two sides are equivalent in their mathematical interpretation. The != operator is the negation.