vstd::std_specs::ops

Trait SubSpecImpl

Source 
pub trait SubSpecImpl<Rhs = Self>: Sub<Rhs> {
    // Required methods
    exec fn obeys_sub_spec() -> bool;
    exec fn sub_req(self, rhs: Rhs) -> bool
       where Self: Sized;
    exec fn sub_spec(self, rhs: Rhs) -> Self::Output
       where Self: Sized;
}

Required Methods§

Source

exec fn obeys_sub_spec() -> bool

Source

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

Source

exec fn sub_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 SubSpecImpl for i8

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as i8 == (self - rhs) }
Source§

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

{ (self - rhs) as i8 }
Source§

impl SubSpecImpl for i16

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as i16 == (self - rhs) }
Source§

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

{ (self - rhs) as i16 }
Source§

impl SubSpecImpl for i32

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as i32 == (self - rhs) }
Source§

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

{ (self - rhs) as i32 }
Source§

impl SubSpecImpl for i64

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as i64 == (self - rhs) }
Source§

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

{ (self - rhs) as i64 }
Source§

impl SubSpecImpl for i128

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as i128 == (self - rhs) }
Source§

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

{ (self - rhs) as i128 }
Source§

impl SubSpecImpl for isize

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as isize == (self - rhs) }
Source§

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

{ (self - rhs) as isize }
Source§

impl SubSpecImpl for u8

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as u8 == (self - rhs) }
Source§

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

{ (self - rhs) as u8 }
Source§

impl SubSpecImpl for u16

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as u16 == (self - rhs) }
Source§

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

{ (self - rhs) as u16 }
Source§

impl SubSpecImpl for u32

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as u32 == (self - rhs) }
Source§

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

{ (self - rhs) as u32 }
Source§

impl SubSpecImpl for u64

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as u64 == (self - rhs) }
Source§

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

{ (self - rhs) as u64 }
Source§

impl SubSpecImpl for u128

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as u128 == (self - rhs) }
Source§

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

{ (self - rhs) as u128 }
Source§

impl SubSpecImpl for usize

Source§

open spec fn obeys_sub_spec() -> bool

{ true }
Source§

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

{ (self - rhs) as usize == (self - rhs) }
Source§

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

{ (self - rhs) as usize }

Implementors§