Type Alias vstd::rwlock::RwLockToks::reader_multiset

pub type reader_multiset<K, V, Pred: InvariantPredicate<K, V>> = MultisetToken<V, reader<K, V, Pred>>;

Aliased Type

struct reader_multiset<K, V, Pred: InvariantPredicate<K, V>> { /* private fields */ }

Implementations

impl<Element, Token> MultisetToken<Element, Token>

where Token: ElementToken<Element>,

pub fn instance_id(self) -> InstanceId

// verusdoc_special_attr modes
// { "fn_mode": "closed spec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }

pub fn multiset(self) -> Multiset<Element>

// verusdoc_special_attr modes
// { "fn_mode": "closed spec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }

pub fn empty(instance_id: InstanceId) -> Self

// verusdoc_special_attr modes
// { "fn_mode": "proof", "ret_mode": "Tracked", "param_modes": ["Default"], "broadcast": false, "ret_name": "s" }

// verusdoc_special_attr ensures
s.instance_id() == instance_id,

// verusdoc_special_attr ensures
s.multiset() === Multiset::empty(),

pub fn insert(&mut self, token: Token)

// verusdoc_special_attr modes
// { "fn_mode": "proof", "ret_mode": "Default", "param_modes": ["Tracked","Tracked"], "broadcast": false, "ret_name": "" }

// verusdoc_special_attr requires
old(self).instance_id() == token.instance_id(),

// verusdoc_special_attr ensures
self.instance_id() == old(self).instance_id(),

// verusdoc_special_attr ensures
self.multiset() == old(self).multiset().insert(token.element()),

pub fn remove(&mut self, element: Element) -> Token

// verusdoc_special_attr modes
// { "fn_mode": "proof", "ret_mode": "Tracked", "param_modes": ["Tracked","Default"], "broadcast": false, "ret_name": "token" }

// verusdoc_special_attr requires
old(self).multiset().contains(element),

// verusdoc_special_attr ensures
self.instance_id() == old(self).instance_id(),

// verusdoc_special_attr ensures
self.multiset() == old(self).multiset().remove(element),

// verusdoc_special_attr ensures
token.instance_id() == self.instance_id(),

// verusdoc_special_attr ensures
token.element() == element,