Trait MonotonicCountToken 

pub trait MonotonicCountToken: Sized {
    // Required methods
    fn instance_id(&self) -> Loc;
    fn count(&self) -> nat;
    fn weaken(&self, count: nat) -> Self;
    fn arbitrary() -> Self;
}

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

VerusSync Strategy	Field type	Token trait
persistent_count	nat	MonotonicCountToken + Copy

A token represents a “lower bound” on the field value, which increases monotonically.

Required Methods

fn instance_id(&self) -> Loc

fn count(&self) -> nat

fn weaken(&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