Skip to main content

StepSpecImpl

vstd::std_specs::iter

Trait StepSpecImpl 

Source 
pub trait StepSpecImpl:
    Clone
    + PartialOrd
    + Sized
    + Step {
    // Required methods
    exec fn spec_is_lt(self, other: Self) -> bool;
    exec fn spec_steps_between(self, end: Self) -> Option<usize>;
    exec fn spec_steps_between_int(self, end: Self) -> int;
    exec fn spec_forward_checked(self, count: usize) -> Option<Self>;
    exec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
    exec fn spec_backward_checked(self, count: usize) -> Option<Self>;
    exec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
}

Required Methods§

Source

exec fn spec_is_lt(self, other: Self) -> bool

Source

exec fn spec_steps_between(self, end: Self) -> Option<usize>

Source

exec fn spec_steps_between_int(self, end: Self) -> int

Source

exec fn spec_forward_checked(self, count: usize) -> Option<Self>

Source

exec fn spec_forward_checked_int(self, count: int) -> Option<Self>

Source

exec fn spec_backward_checked(self, count: usize) -> Option<Self>

Source

exec fn spec_backward_checked_int(self, count: int) -> Option<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 StepSpecImpl for i8

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i8::MAX { Some((self + count) as i8) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i8::MIN { Some((self - count) as i8) } else { None } }
Source§

impl StepSpecImpl for i16

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i16::MAX { Some((self + count) as i16) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i16::MIN { Some((self - count) as i16) } else { None } }
Source§

impl StepSpecImpl for i32

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i32::MAX { Some((self + count) as i32) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i32::MIN { Some((self - count) as i32) } else { None } }
Source§

impl StepSpecImpl for i64

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i64::MAX { Some((self + count) as i64) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i64::MIN { Some((self - count) as i64) } else { None } }
Source§

impl StepSpecImpl for i128

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i128::MAX { Some((self + count) as i128) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i128::MIN { Some((self - count) as i128) } else { None } }
Source§

impl StepSpecImpl for isize

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= isize::MAX { Some((self + count) as isize) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= isize::MIN { Some((self - count) as isize) } else { None } }
Source§

impl StepSpecImpl for u8

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u8::MAX { Some((self + count) as u8) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u8::MIN { Some((self - count) as u8) } else { None } }
Source§

impl StepSpecImpl for u16

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u16::MAX { Some((self + count) as u16) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u16::MIN { Some((self - count) as u16) } else { None } }
Source§

impl StepSpecImpl for u32

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u32::MAX { Some((self + count) as u32) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u32::MIN { Some((self - count) as u32) } else { None } }
Source§

impl StepSpecImpl for u64

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u64::MAX { Some((self + count) as u64) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u64::MIN { Some((self - count) as u64) } else { None } }
Source§

impl StepSpecImpl for u128

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u128::MAX { Some((self + count) as u128) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u128::MIN { Some((self - count) as u128) } else { None } }
Source§

impl StepSpecImpl for usize

Source§

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }
Source§

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}
Source§

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }
Source§

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_forward_checked_int(self, count as int) }
Source§

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= usize::MAX { Some((self + count) as usize) } else { None } }
Source§

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ StepSpec::spec_backward_checked_int(self, count as int) }
Source§

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= usize::MIN { Some((self - count) as usize) } else { None } }

Implementors§