Trait ElementToken 

pub trait ElementToken<Element>: Sized {
    // Required methods
    fn instance_id(&self) -> Loc;
    fn element(&self) -> Element;
    fn arbitrary() -> Self;
}

Interface for VerusSync tokens created for a field marked with the set, persistent_set or multiset strategies.

VerusSync Strategy	Field type	Token trait
set	Set<V>	UniqueElementToken<V>
iset	ISet<V>	UniqueElementToken<V>
persistent_set	Set<V>	ElementToken<V> + Copy
persistent_iset	ISet<V>	ElementToken<V> + Copy
multiset	Multiset<V>	ElementToken<V>

Each token represents a single element of the set or multiset.

• For the set strategy, the token for any given element is unique.
• For the persistent_set strategy, the token for any given element is not unique, but is Copy.
• For the multiset strategy, the tokens are neither unique nor Copy, as the specific multiplicity of each element must be exact.

To work with a collection of ElementTokens, use [SetToken] or [MultisetToken].

Required Methods

fn instance_id(&self) -> Loc

fn element(&self) -> Element

fn arbitrary() -> Self

Return an arbitrary token. It’s not possible to do anything interesting with this token because it doesn’t have a specified instance.

Dyn Compatibility

This trait is not dyn compatible.

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

Implementors

impl<K, V, Pred> ElementToken<()> for pending_reader<K, V, Pred>

where Pred: InvariantPredicate<K, V>,

impl<K, V, Pred> ElementToken<V> for reader<K, V, Pred>

where Pred: InvariantPredicate<K, V>,