Struct vstd::rwlock::RwLockToks::flag_exc
source · pub struct flag_exc<K, V, Pred: InvariantPredicate<K, V>> { /* private fields */ }
Trait Implementations§
source§impl<V, Pred: RwLockPredicate<V>> AtomicInvariantPredicate<Tracked<Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>, bool, flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>> for InvariantPredicate_auto_RwLock_exc
impl<V, Pred: RwLockPredicate<V>> AtomicInvariantPredicate<Tracked<Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>, bool, flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>> for InvariantPredicate_auto_RwLock_exc
source§open spec fn atomic_inv(
declare_struct_with_invariants_tmp_k: FieldType_RwLock_inst<V, Pred>,
declare_struct_with_invariants_tmp_v: bool,
declare_struct_with_invariants_tmp_g: flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>
) -> bool
open spec fn atomic_inv( declare_struct_with_invariants_tmp_k: FieldType_RwLock_inst<V, Pred>, declare_struct_with_invariants_tmp_v: bool, declare_struct_with_invariants_tmp_g: flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>> ) -> bool
{
let inst = declare_struct_with_invariants_tmp_k;
let v = declare_struct_with_invariants_tmp_v;
let g = declare_struct_with_invariants_tmp_g;
{ g.instance_id() == inst@.id() && g.value() == v }
}
source§impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<bool> for flag_exc<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<bool> for flag_exc<K, V, Pred>
Auto Trait Implementations§
impl<K, V, Pred> Freeze for flag_exc<K, V, Pred>
impl<K, V, Pred> RefUnwindSafe for flag_exc<K, V, Pred>
impl<K, V, Pred> Send for flag_exc<K, V, Pred>
impl<K, V, Pred> Sync for flag_exc<K, V, Pred>
impl<K, V, Pred> Unpin for flag_exc<K, V, Pred>
impl<K, V, Pred> UnwindSafe for flag_exc<K, V, Pred>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more