pub trait UniqueValueToken<Value>: ValueToken<Value> {
// Required method
proof fn unique(tracked &mut self, tracked other: &Self);
}Expand description
Interface for VerusSync tokens created for a field marked with the variable or option strategies.
See the super-trait ValueToken for more information.
Required Methods§
Sourceproof fn unique(tracked &mut self, tracked other: &Self)
proof fn unique(tracked &mut self, tracked other: &Self)
ensures
self.instance_id() != other.instance_id(),*self == *old(self),The token for a given instance must be unique; in other words, if we have two tokens, they must be for distinct instances. 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", so this trait is not object safe.