Trait DivSpecImpl

Source
pub trait DivSpecImpl<Rhs = Self>: Div<Rhs> {
    // Required methods
    exec fn obeys_div_spec() -> bool;
    exec fn div_req(self, rhs: Rhs) -> bool
       where Self: Sized;
    exec fn div_spec(self, rhs: Rhs) -> Self::Output
       where Self: Sized;
}

Required Methods§

Source

exec fn obeys_div_spec() -> bool

Source

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

Source

exec fn div_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§

Source§

impl DivSpecImpl for i8

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == i8::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as i8 } else { (-((-self) / (rhs as int))) as i8 } }
Source§

impl DivSpecImpl for i16

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == i16::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as i16 } else { (-((-self) / (rhs as int))) as i16 } }
Source§

impl DivSpecImpl for i32

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == i32::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as i32 } else { (-((-self) / (rhs as int))) as i32 } }
Source§

impl DivSpecImpl for i64

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == i64::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as i64 } else { (-((-self) / (rhs as int))) as i64 } }
Source§

impl DivSpecImpl for i128

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == i128::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as i128 } else { (-((-self) / (rhs as int))) as i128 } }
Source§

impl DivSpecImpl for isize

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 && !(self == isize::MIN && rhs == -1) }
Source§

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

{ if self >= 0 { (self / rhs) as isize } else { (-((-self) / (rhs as int))) as isize } }
Source§

impl DivSpecImpl for u8

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }
Source§

impl DivSpecImpl for u16

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }
Source§

impl DivSpecImpl for u32

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }
Source§

impl DivSpecImpl for u64

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }
Source§

impl DivSpecImpl for u128

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }
Source§

impl DivSpecImpl for usize

Source§

open spec fn obeys_div_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ self / rhs }

Implementors§