pub trait StepSpecwhere
Self: Sized,{
// Required methods
spec fn spec_is_lt(self, other: Self) -> bool;
spec fn spec_steps_between(self, end: Self) -> Option<usize>;
spec fn spec_steps_between_int(self, end: Self) -> int;
spec fn spec_forward_checked(self, count: usize) -> Option<Self>;
spec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
spec fn spec_backward_checked(self, count: usize) -> Option<Self>;
spec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
}Required Methods§
Sourcespec fn spec_is_lt(self, other: Self) -> bool
spec fn spec_is_lt(self, other: Self) -> bool
Sourcespec fn spec_steps_between(self, end: Self) -> Option<usize>
spec fn spec_steps_between(self, end: Self) -> Option<usize>
Sourcespec fn spec_steps_between_int(self, end: Self) -> int
spec fn spec_steps_between_int(self, end: Self) -> int
Sourcespec fn spec_forward_checked(self, count: usize) -> Option<Self>
spec fn spec_forward_checked(self, count: usize) -> Option<Self>
Sourcespec fn spec_forward_checked_int(self, count: int) -> Option<Self>
spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
Sourcespec fn spec_backward_checked(self, count: usize) -> Option<Self>
spec fn spec_backward_checked(self, count: usize) -> Option<Self>
Sourcespec fn spec_backward_checked_int(self, count: int) -> Option<Self>
spec 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 StepSpec for i8
impl StepSpec for i8
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for i16
impl StepSpec for i16
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for i32
impl StepSpec for i32
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for i64
impl StepSpec for i64
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for i128
impl StepSpec for i128
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for isize
impl StepSpec for isize
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for u8
impl StepSpec for u8
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for u16
impl StepSpec for u16
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for u32
impl StepSpec for u32
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for u64
impl StepSpec for u64
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for u128
impl StepSpec for u128
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
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 StepSpec for usize
impl StepSpec for usize
Source§open spec fn spec_is_lt(self, other: Self) -> bool
open spec fn spec_is_lt(self, other: Self) -> bool
{ self < other }Source§open spec fn spec_steps_between(self, end: Self) -> Option<usize>
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
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>
open spec fn spec_forward_checked(self, count: usize) -> Option<Self>
{ self.spec_forward_checked_int(count as int) }Source§open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>
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>
open spec fn spec_backward_checked(self, count: usize) -> Option<Self>
{ self.spec_backward_checked_int(count as int) }Source§open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>
{ if self - count >= usize::MIN { Some((self - count) as usize) } else { None } }