Struct nat
pub struct nat;
Trait Implementations§
§impl Ord for nat
impl Ord for nat
§impl PartialOrd for nat
impl PartialOrd for nat
§impl SpecEuclideanDiv for nat
impl SpecEuclideanDiv for nat
type Output = nat
fn spec_euclidean_div(self, _rhs: nat) -> <nat as SpecEuclideanDiv>::Output
§impl SpecEuclideanMod for nat
impl SpecEuclideanMod for nat
type Output = nat
fn spec_euclidean_mod(self, _rhs: nat) -> <nat as SpecEuclideanMod>::Output
Source§impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<nat> for flag_rc<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<nat> for flag_rc<K, V, Pred>
Source§impl<K, V, Pred: InvariantPredicate<K, V>> ValueToken<nat> for flag_rc<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> ValueToken<nat> for flag_rc<K, V, Pred>
impl Copy for nat
impl Eq for nat
impl Structural for nat
Auto Trait Implementations§
impl Freeze for nat
impl RefUnwindSafe for nat
impl Send for nat
impl Sync for nat
impl Unpin for nat
impl UnwindSafe for nat
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<VERUS_SPEC__A> OrdSpec for VERUS_SPEC__A
impl<VERUS_SPEC__A> OrdSpec for VERUS_SPEC__A
Source§exec fn obeys_cmp_spec() -> bool
exec fn obeys_cmp_spec() -> bool
Source§exec fn cmp_spec(&self, other: &VERUS_SPEC__A) -> Ordering
exec fn cmp_spec(&self, other: &VERUS_SPEC__A) -> Ordering
Source§impl<A, Rhs> PartialEqIs<Rhs> for A
impl<A, Rhs> PartialEqIs<Rhs> for A
Source§impl<Rhs, VERUS_SPEC__A> PartialEqSpec<Rhs> for VERUS_SPEC__A
impl<Rhs, VERUS_SPEC__A> PartialEqSpec<Rhs> for VERUS_SPEC__A
Source§impl<A, Rhs> PartialOrdIs<Rhs> for A
impl<A, Rhs> PartialOrdIs<Rhs> for A
Source§open spec fn is_lt(&self, other: &Rhs) -> bool
open spec fn is_lt(&self, other: &Rhs) -> bool
{ self.partial_cmp_spec(other) == Some(Ordering::Less) }
Source§open spec fn is_le(&self, other: &Rhs) -> bool
open spec fn is_le(&self, other: &Rhs) -> bool
{ matches!(self.partial_cmp_spec(other), Some(Ordering::Less | Ordering::Equal)) }