vstd::std_specs::ops

Trait ShlSpecImpl

pub trait ShlSpecImpl<Rhs = Self>: Shl<Rhs> {
    // Required methods
    exec fn obeys_shl_spec() -> bool;
    exec fn shl_req(self, rhs: Rhs) -> bool
       where Self: Sized;
    exec fn shl_spec(self, rhs: Rhs) -> Self::Output
       where Self: Sized;
}

Required Methods§

exec fn obeys_shl_spec() -> bool

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

exec fn shl_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 ShlSpecImpl for i8

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < i8::BITS }

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

{ self << rhs }

impl ShlSpecImpl for i16

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < i16::BITS }

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

{ self << rhs }

impl ShlSpecImpl for i32

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < i32::BITS }

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

{ self << rhs }

impl ShlSpecImpl for i64

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < i64::BITS }

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

{ self << rhs }

impl ShlSpecImpl for i128

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < i128::BITS }

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

{ self << rhs }

impl ShlSpecImpl for isize

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < isize::BITS }

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

{ self << rhs }

impl ShlSpecImpl for u8

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < u8::BITS }

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

{ self << rhs }

impl ShlSpecImpl for u16

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < u16::BITS }

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

{ self << rhs }

impl ShlSpecImpl for u32

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < u32::BITS }

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

{ self << rhs }

impl ShlSpecImpl for u64

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < u64::BITS }

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

{ self << rhs }

impl ShlSpecImpl for u128

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < u128::BITS }

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

{ self << rhs }

impl ShlSpecImpl for usize

open spec fn obeys_shl_spec() -> bool

{ true }

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

{ rhs < usize::BITS }

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

{ self << rhs }

Implementors§