pub trait ElementToken<Element>: Sized {
// Required methods
spec fn instance_id(&self) -> InstanceId;
spec fn element(&self) -> Element;
proof fn arbitrary() -> tracked s : Self;
}Expand description
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> |
persistent_set | Set<V> | ElementToken<V> + Copy |
multiset | Multiset<V> | ElementToken<V> |
Each token represents a single element of the set or multiset.
- For the
setstrategy, the token for any given element is unique. - For the
persistent_setstrategy, the token for any given element is not unique, but isCopy. - For the
multisetstrategy, the tokens are neither unique norCopy, as the specific multiplicity of each element must be exact.
To work with a collection of ElementTokens, use SetToken or MultisetToken.
Required Methods§
Sourcespec fn instance_id(&self) -> InstanceId
spec fn instance_id(&self) -> InstanceId
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.