Trait ElementToken 

pub trait ElementToken<Element>: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    spec fn element(&self) -> Element;
    proof fn arbitrary() -> tracked s : 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

spec fn instance_id(&self) -> InstanceId

spec fn element(&self) -> Element

proof fn arbitrary() -> tracked s : 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: InvariantPredicate<K, V>> ElementToken<()> for pending_reader<K, V, Pred>

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