vstd::std_specs::ops

Trait BitAndSpecImpl

pub trait BitAndSpecImpl<Rhs = Self>: BitAnd<Rhs> {
    // Required methods
    exec fn obeys_bitand_spec() -> bool;
    exec fn bitand_req(self, rhs: Rhs) -> bool
       where Self: Sized;
    exec fn bitand_spec(self, rhs: Rhs) -> Self::Output
       where Self: Sized;
}

Required Methods§

exec fn obeys_bitand_spec() -> bool

exec fn bitand_req(self, rhs: Rhs) -> bool
where Self: Sized,

exec fn bitand_spec(self, rhs: Rhs) -> Self::Output
where Self: Sized,

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 BitAndSpecImpl for i8

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: i8) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for i16

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: i16) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for i32

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: i32) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for i64

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: i64) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for i128

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: i128) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for isize

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: isize) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for u8

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: u8) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for u16

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: u16) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for u32

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: u32) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for u64

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: u64) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for u128

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: u128) -> Self::Output

{ self & rhs }

impl BitAndSpecImpl for usize

open spec fn obeys_bitand_spec() -> bool

{ true }

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

{ true }

open spec fn bitand_spec(self, rhs: usize) -> Self::Output

{ self & rhs }

Implementors§