Skip to main content

BitAndAssignSpecImpl

vstd::std_specs::ops

Trait BitAndAssignSpecImpl

pub trait BitAndAssignSpecImpl<Rhs = Self>: BitAndAssign<Rhs> {
    // Required methods
    exec fn obeys_bitand_assign_spec() -> bool;
    exec fn bitand_assign_req(&self, rhs: Rhs) -> bool;
    exec fn bitand_assign_spec(&self, rhs: Rhs) -> &Self;
}

Required Methods§

exec fn obeys_bitand_assign_spec() -> bool

exec fn bitand_assign_req(&self, rhs: Rhs) -> bool

exec fn bitand_assign_spec(&self, rhs: Rhs) -> &Self

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.

Implementations on Foreign Types§

impl BitAndAssignSpecImpl for i8

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: i8) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: i8) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for i16

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: i16) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: i16) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for i32

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: i32) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: i32) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for i64

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: i64) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: i64) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for i128

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: i128) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: i128) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for isize

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: isize) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: isize) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for u8

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: u8) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: u8) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for u16

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: u16) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: u16) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for u32

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: u32) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: u32) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for u64

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: u64) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: u64) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for u128

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: u128) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: u128) -> &Self

{ &(self & rhs) }

impl BitAndAssignSpecImpl for usize

open spec fn obeys_bitand_assign_spec() -> bool

{ true }

open spec fn bitand_assign_req(&self, rhs: usize) -> bool

{ true }

open spec fn bitand_assign_spec(&self, rhs: usize) -> &Self

{ &(self & rhs) }

Implementors§