Skip to main content

ExBitOrAssign

vstd::std_specs::ops

Trait ExBitOrAssign 

Source 
pub trait ExBitOrAssign<Rhs = Self> {
    type ExternalTraitSpecificationFor: BitOrAssign<Rhs>;

    // Required methods
    spec fn obeys_bitor_assign_spec() -> bool;
    spec fn bitor_assign_req(&self, rhs: Rhs) -> bool;
    spec fn bitor_assign_spec(&self, rhs: Rhs) -> &Self;
    exec fn bitor_assign(&mut self, rhs: Rhs);
}

Required Associated Types§

Source

type ExternalTraitSpecificationFor: BitOrAssign<Rhs>

Required Methods§

Source

spec fn obeys_bitor_assign_spec() -> bool

Source

spec fn bitor_assign_req(&self, rhs: Rhs) -> bool

Source

spec fn bitor_assign_spec(&self, rhs: Rhs) -> &Self

Source

exec fn bitor_assign(&mut self, rhs: Rhs)

requires
self.bitor_assign_req(rhs),
ensures
Self::obeys_bitor_assign_spec() ==> &*final(self) == old(self).bitor_assign_spec(rhs),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§