Skip to main content

DivAssignSpecImpl

Trait DivAssignSpecImpl 

Source
pub trait DivAssignSpecImpl<Rhs = Self>: DivAssign<Rhs> {
    // Required methods
    exec fn obeys_div_assign_spec() -> bool;
    exec fn div_assign_req(&self, rhs: Rhs) -> bool;
    exec fn div_assign_spec(&self, rhs: Rhs) -> &Self;
}

Required Methods§

Source

exec fn obeys_div_assign_spec() -> bool

Source

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

Source

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

Source§

impl DivAssignSpecImpl for i8

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as i8) }
Source§

impl DivAssignSpecImpl for i16

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as i16) }
Source§

impl DivAssignSpecImpl for i32

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as i32) }
Source§

impl DivAssignSpecImpl for i64

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as i64) }
Source§

impl DivAssignSpecImpl for i128

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as i128) }
Source§

impl DivAssignSpecImpl for isize

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

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

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

{ &(super::super::arithmetic::div_mod::rust_div(self as int, rhs as int) as isize) }
Source§

impl DivAssignSpecImpl for u8

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }
Source§

impl DivAssignSpecImpl for u16

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }
Source§

impl DivAssignSpecImpl for u32

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }
Source§

impl DivAssignSpecImpl for u64

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }
Source§

impl DivAssignSpecImpl for u128

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }
Source§

impl DivAssignSpecImpl for usize

Source§

open spec fn obeys_div_assign_spec() -> bool

{ true }
Source§

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

{ rhs != 0 }
Source§

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

{ &(self / rhs) }

Implementors§