Trait vstd::tokens::SimpleToken

pub trait SimpleToken: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    proof fn arbitrary() -> tracked s : Self;
}

Expand description

Interface for VerusSync tokens created for a field marked with the bool or persistent_bool strategy.

VerusSync Strategy	Field type	Token trait
`bool`	`bool`	`UniqueSimpleToken<V>`
`persistent_bool`	`bool`	`SimpleToken<V> + Copy`

The token contains no additional data; its presence indicates that the boolean field is true.

Required Methods§

Return an arbitrary token. It’s not possible to do anything interesting with this token because it doesn’t have a specified instance.

This trait is not object safe.