The has operator

Syntax

has_expr ::= spec_expr  has spec_expr
           | spec_expr !has spec_expr

Desugaring

In spec code, the expression expr1 has expr2 desguars to expr1.spec_has(expr2), which is resolved as normal via Rust’s standard method resolution.

Likewise, the expression expr1 !has expr2 desugars to !expr1.spec_has(expr2).

Examples

We typically use the has operator to indicate that a collection contains a particular element. The vstd library provides several container types with spec_has functions defined, e.g., Set::spec_has and Multiset::spec_has.

Example:

proof fn test_set() {
    let s: Set<int> = set![1, 2];
    assert(s has 1);
    assert(s has 2);
    assert(s !has 3);
}

proof fn test_multiset() {
    let s: Multiset<int> = Multiset::empty().insert(1).insert(1).insert(2);
    assert(s has 1);
    assert(s has 2);
    assert(s !has 3);
}