Trait vstd::tokens::UniqueElementToken

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

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

See the super-trait ElementToken for more information.

Required Methods§

source

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

ensures
self.instance_id() == other.instance_id() ==> self.element() != other.element(),
*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.

Object Safety§

This trait is not object safe.

Implementors§