Trait CountToken 

pub trait CountToken: Sized {
    // Required methods
    fn instance_id(&self) -> Loc;
    fn count(&self) -> nat;
    fn join(&mut self, other: Self);
    fn split(&mut self, count: nat) -> Self;
    fn weaken_shared(&self, count: nat) -> &Self;
    fn arbitrary() -> Self;
}

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

VerusSync Strategy	Field type	Token trait
count	nat	CountToken

These tokens are “fungible” in the sense that they can be combined and split, numbers combining additively.

(For the persistent_count strategy, see MonotonicCountToken.)

Required Methods

fn instance_id(&self) -> Loc

fn count(&self) -> nat

fn join(&mut self, other: Self)

fn split(&mut self, count: nat) -> Self

fn weaken_shared(&self, count: nat) -> &Self

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