Trait UniqueElementToken 

pub trait UniqueElementToken<Element>: ElementToken<Element> {
    // Required method
    proof fn unique(tracked &mut self, tracked other: &Self);
}

Interface for VerusSync tokens created for a field marked with the set strategy.

See the super-trait ElementToken for more information.

Required Methods

proof fn unique(tracked &mut self, tracked other: &Self)

ensures

final(self).instance_id() == other.instance_id()
    ==> final(self).element() != other.element(),

*final(self) == *old(self),

The token for a given instance and element must be unique; in other words, if we have two tokens, they must be for distinct instances or elements. Though the first argument is mutable, the value is not really mutated; this is only used to ensure unique ownership of the argument.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors