vstd::std_specs::ops

Trait ShrSpecImpl

pub trait ShrSpecImpl<Rhs = Self>: Shr<Rhs> {
    // Required methods
    exec fn obeys_shr_spec() -> bool;
    exec fn shr_req(self, rhs: Rhs) -> bool
       where Self: Sized;
    exec fn shr_spec(self, rhs: Rhs) -> Self::Output
       where Self: Sized;
}

Required Methods§

exec fn obeys_shr_spec() -> bool

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

exec fn shr_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 ShrSpecImpl for i8

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < i8::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for i16

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < i16::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for i32

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < i32::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for i64

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < i64::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for i128

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < i128::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for isize

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < isize::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for u8

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < u8::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for u16

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < u16::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for u32

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < u32::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for u64

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < u64::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for u128

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < u128::BITS }

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

{ self >> rhs }

impl ShrSpecImpl for usize

open spec fn obeys_shr_spec() -> bool

{ true }

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

{ rhs < usize::BITS }

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

{ self >> rhs }

Implementors§