Struct Page Flags &nbsp; Copy item path

impl PageFlags

pub open spec fn flags_spec(&self) -> Set<__ghostPageFlags>

{ Self::flags_from_bits(self.bits()) }

pub open spec fn flags_from_bits(bits: u8) -> Set<__ghostPageFlags>

{
    ::vstd::set::Set::<
        __ghostPageFlags,
    >::from_finite_type(|flag: __ghostPageFlags| {
        flag.enabled() && (bits & flag.bit()) == flag.bit()
    })
}

pub closed spec fn R_spec() -> Self

pub const exec fn R() -> r : Self

ensures

r.bits() == (0b00000001),

r.flags_spec() == Self::flags_from_bits((0b00000001) as u8),

returns

Self::R_spec(),

Readable.

pub closed spec fn W_spec() -> Self

pub const exec fn W() -> r : Self

ensures

r.bits() == (0b00000010),

r.flags_spec() == Self::flags_from_bits((0b00000010) as u8),

returns

Self::W_spec(),

Writable.

pub closed spec fn X_spec() -> Self

pub const exec fn X() -> r : Self

ensures

r.bits() == (0b00000100),

r.flags_spec() == Self::flags_from_bits((0b00000100) as u8),

returns

Self::X_spec(),

Executable.

pub closed spec fn RW_spec() -> Self

pub const exec fn RW() -> r : Self

ensures

r.bits() == (0b00000011),

r.flags_spec() == Self::flags_from_bits((0b00000011) as u8),

returns

Self::RW_spec(),

Readable + writable.

pub closed spec fn RX_spec() -> Self

pub const exec fn RX() -> r : Self

ensures

r.bits() == (0b00000101),

r.flags_spec() == Self::flags_from_bits((0b00000101) as u8),

returns

Self::RX_spec(),

Readable + executable.

pub closed spec fn RWX_spec() -> Self

pub const exec fn RWX() -> r : Self

ensures

r.bits() == (0b00000111),

r.flags_spec() == Self::flags_from_bits((0b00000111) as u8),

returns

Self::RWX_spec(),

Readable + writable + executable.

pub closed spec fn ACCESSED_spec() -> Self

pub const exec fn ACCESSED() -> r : Self

ensures

r.bits() == (0b00001000),

r.flags_spec() == Self::flags_from_bits((0b00001000) as u8),

returns

Self::ACCESSED_spec(),

Has the memory page been read or written.

pub closed spec fn DIRTY_spec() -> Self

pub const exec fn DIRTY() -> r : Self

ensures

r.bits() == (0b00010000),

r.flags_spec() == Self::flags_from_bits((0b00010000) as u8),

returns

Self::DIRTY_spec(),

Has the memory page been written.

pub closed spec fn AVAIL1_spec() -> Self

pub const exec fn AVAIL1() -> r : Self

ensures

r.bits() == (0b01000000),

r.flags_spec() == Self::flags_from_bits((0b01000000) as u8),

returns

Self::AVAIL1_spec(),

The first bit available for software use.

pub closed spec fn AVAIL2_spec() -> Self

pub const exec fn AVAIL2() -> r : Self

ensures

r.bits() == (0b10000000),

r.flags_spec() == Self::flags_from_bits((0b10000000) as u8),

returns

Self::AVAIL2_spec(),

The second bit available for software use.

pub proof fn lemma_all_constant()

ensures

Self::all().bits() == Self::all_spec().bits_spec(),

Self::all_spec().bits_spec()
    == (0 as u8)
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable."]) true
        } {
            ((0b00000001) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Writable."]) true
        } {
            ((0b00000010) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Executable."]) true
        } {
            ((0b00000100) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable."]) true
        } {
            ((0b00000011) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + executable."]) true
        } {
            ((0b00000101) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable + executable."]) true
        } {
            ((0b00000111) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been read or written."]) true
        } {
            ((0b00001000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been written."]) true
        } {
            ((0b00010000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The first bit available for software use."]) true
        } {
            ((0b01000000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The second bit available for software use."]) true
        } {
            ((0b10000000) as u8)
        } else {
            0 as u8
        }),

Self::all().bits()
    == (0 as u8)
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable."]) true
        } {
            ((0b00000001) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Writable."]) true
        } {
            ((0b00000010) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Executable."]) true
        } {
            ((0b00000100) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable."]) true
        } {
            ((0b00000011) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + executable."]) true
        } {
            ((0b00000101) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable + executable."]) true
        } {
            ((0b00000111) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been read or written."]) true
        } {
            ((0b00001000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been written."]) true
        } {
            ((0b00010000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The first bit available for software use."]) true
        } {
            ((0b01000000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The second bit available for software use."]) true
        } {
            ((0b10000000) as u8)
        } else {
            0 as u8
        }),

pub broadcast proof fn lemma_consts()

ensures

Self::all().bits()
    == (0 as u8)
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable."]) true
        } {
            ((0b00000001) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Writable."]) true
        } {
            ((0b00000010) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Executable."]) true
        } {
            ((0b00000100) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable."]) true
        } {
            ((0b00000011) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + executable."]) true
        } {
            ((0b00000101) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Readable + writable + executable."]) true
        } {
            ((0b00000111) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been read or written."]) true
        } {
            ((0b00001000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" Has the memory page been written."]) true
        } {
            ((0b00010000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The first bit available for software use."]) true
        } {
            ((0b01000000) as u8)
        } else {
            0 as u8
        })
        | (if $crate::__bitflags_cfg_expr! {
            (#[doc = r" The second bit available for software use."]) true
        } {
            ((0b10000000) as u8)
        } else {
            0 as u8
        }),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Readable."]) Self::R().bits() == ((0b00000001) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Writable."]) Self::W().bits() == ((0b00000010) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Executable."]) Self::X().bits() == ((0b00000100) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Readable + writable."]) Self::RW().bits() == ((0b00000011) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Readable + executable."]) Self::RX().bits() == ((0b00000101) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Readable + writable + executable."]) Self::RWX().bits() == ((0b00000111)
    as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Has the memory page been read or written."]) Self::ACCESSED().bits() ==
    ((0b00001000) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" Has the memory page been written."]) Self::DIRTY().bits() ==
    ((0b00010000) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" The first bit available for software use."]) Self::AVAIL1().bits() ==
    ((0b01000000) as u8)
),

$crate::__bitflags_cfg_guarded_expr!(
    (#[doc = r" The second bit available for software use."]) Self::AVAIL2().bits() ==
    ((0b10000000) as u8)
),

pub proof fn lemma_from_bits_bits(bits: u8)

requires

bits & Self::all().bits() == bits,

ensures

Self::from_bits(bits)->0.bits() == bits,

pub proof fn lemma_eq_from_bits(left: Self, right: Self)

requires

left.bits() == right.bits(),

ensures

left == right,

pub closed spec fn bits_spec(&self) -> u8

The raw bits stored inside this flags value.

pub const exec fn bits(&self) -> u8

returns

self.bits(),

pub closed spec fn empty_spec() -> Self

pub const exec fn empty() -> r : Self

ensures

r.bits() == 0,

r.flags_spec() == Self::flags_from_bits(0),

returns

Self::empty(),

pub closed spec fn all_spec() -> Self

pub const exec fn all() -> r : Self

ensures

r == Self::all_spec(),

r.bits() == Self::all().bits(),

r.flags_spec() == Self::flags_from_bits(Self::all().bits()),

pub closed spec fn known_bits_spec(&self) -> u8

The bits in self that correspond to declared flags.

pub const exec fn known_bits(&self) -> r : u8

returns

self.known_bits(),

pub closed spec fn unknown_bits_spec(&self) -> u8

The bits in self that do not correspond to declared flags.

pub const exec fn unknown_bits(&self) -> r : u8

returns

self.unknown_bits(),

pub open spec fn contains_unknown_bits_spec(&self) -> bool

{ self.unknown_bits() != 0 }

This method returns true if any unknown bits are set.

pub const exec fn contains_unknown_bits(&self) -> r : bool

returns

self.contains_unknown_bits(),

pub open spec fn is_empty_spec(&self) -> bool

{ self.bits() == 0 }

Whether all bits in self are unset.

pub const exec fn is_empty(&self) -> r : bool

returns

self.is_empty(),

pub open spec fn is_all_spec(&self) -> bool

{ Self::all().bits() | self.bits() == self.bits() }

Whether all known bits are set.

pub const exec fn is_all(&self) -> r : bool

returns

self.is_all(),

pub open spec fn contains_spec(&self, other: Self) -> bool

{ (self.bits() & other.bits()) == other.bits() }

Whether all set bits in other are also set in self.

pub open spec fn contains_flags_spec(&self, other: Self) -> bool

{ self.contains(other) }

pub const exec fn contains(&self, other: Self) -> r : bool

returns

self.contains(other),

pub open spec fn intersects_spec(&self, other: Self) -> bool

{ (self.bits() & other.bits()) != 0 }

Whether any set bits in other are also set in self.

pub const exec fn intersects(&self, other: Self) -> r : bool

returns

self.intersects(other),

pub closed spec fn from_bits_truncate_spec(bits: u8) -> Self

pub closed spec fn from_bits_retain_spec(bits: u8) -> Self

pub const exec fn from_bits_retain(bits: u8) -> r : Self

ensures

r.bits() == bits,

r.flags_spec() == Self::flags_from_bits(bits),

returns

Self::from_bits_retain(bits),

pub exec fn from_name(name: &str) -> r : Option<Self>

ensures

r matches Some(
    flags_value,
) ==> {
    &&& flags_value.flags_spec() == Self::flags_from_bits(flags_value.bits())

},

Get a flags value with the bits of a flag with the given name set.

This method will return None if name is empty or doesn’t correspond to any named flag.

pub const exec fn from_bits_truncate(bits: u8) -> r : Self

ensures

r.bits() == (bits & Self::all().bits()),

r.flags_spec() == Self::flags_from_bits(bits & Self::all().bits()),

returns

Self::from_bits_truncate(bits),

pub closed spec fn from_bits_spec(bits: u8) -> Option<Self>

pub const exec fn from_bits(bits: u8) -> r : Option<Self>

ensures

r is Some == ((bits & Self::all().bits()) == bits),

r matches Some(
    flags_value,
) ==> {
    &&& flags_value.bits() == bits
    &&& flags_value.flags_spec() == Self::flags_from_bits(bits)

},

returns

Self::from_bits(bits),

pub closed spec fn remove_spec(self, other: Self) -> Self

pub exec fn insert(&mut self, other: Self)

ensures

final(self).bits() == (old(self).bits() | other.bits()),

final(self).flags_spec() == Self::flags_from_bits(old(self).bits() | other.bits()),

pub exec fn remove(&mut self, other: Self)

ensures

*final(self) == old(self).remove_spec(other),

final(self).bits() == (old(self).bits() & !other.bits()),

final(self).flags_spec() == Self::flags_from_bits(old(self).bits() & !other.bits()),

pub exec fn toggle(&mut self, other: Self)

ensures

final(self).bits() == (old(self).bits() ^ other.bits()),

final(self).flags_spec() == Self::flags_from_bits(old(self).bits() ^ other.bits()),

The bitwise exclusive-or (^) of the bits in self and other.

pub exec fn set(&mut self, other: Self, value: bool)

ensures

value ==> final(self).bits() == (old(self).bits() | other.bits()),

!value ==> final(self).bits() == (old(self).bits() & !other.bits()),

Call insert when value is true or remove when value is false.

pub exec fn truncate(&mut self)

ensures

final(self).bits() == (old(self).bits() & Self::all().bits()),

final(self).flags_spec() == Self::flags_from_bits(old(self).bits() & Self::all().bits()),

Remove any unknown bits from the flags.

pub exec fn clear(&mut self)

ensures

final(self).bits() == 0,

final(self).flags_spec() == Self::flags_from_bits(0),

Unsets all bits in the flags.

pub closed spec fn union_spec(self, other: Self) -> Self

pub const exec fn union(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() | other.bits()),

returns

self.union(other),

pub closed spec fn intersection_spec(self, other: Self) -> Self

pub const exec fn intersection(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() & other.bits()),

returns

self.intersection(other),

pub closed spec fn difference_spec(self, other: Self) -> Self

pub const exec fn difference(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() & !other.bits()),

returns

self.difference(other),

pub closed spec fn symmetric_difference_spec(self, other: Self) -> Self

pub const exec fn symmetric_difference(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() ^ other.bits()),

returns

self.symmetric_difference(other),

pub closed spec fn complement_spec(self) -> Self

pub const exec fn complement(self) -> r : Self

ensures

r.bits() == (!self.bits() & Self::all().bits()),

r.flags_spec() == Self::flags_from_bits(!self.bits() & Self::all().bits()),

returns

self.complement(),

Trait Implementations§

impl BitAnd for PageFlags

exec fn bitand(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() & other.bits()),

type Output = PageFlags

The resulting type after applying the & operator.

impl BitAndAssign for PageFlags

fn bitand_assign(&mut self, other: Self)

Performs the &= operation. Read more

impl BitAndSpecImpl for PageFlags

open spec fn obeys_bitand_spec() -> bool

{ true }

open spec fn bitand_req(self, rhs: Self) -> bool

{ true }

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

{ self.intersection(rhs) }

impl BitOr for PageFlags

exec fn bitor(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() | other.bits()),

type Output = PageFlags

The resulting type after applying the | operator.

impl BitOrAssign for PageFlags

fn bitor_assign(&mut self, other: Self)

Performs the |= operation. Read more

impl BitOrSpecImpl for PageFlags

open spec fn obeys_bitor_spec() -> bool

{ true }

open spec fn bitor_req(self, rhs: Self) -> bool

{ true }

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

{ self.union(rhs) }

impl BitXor for PageFlags

exec fn bitxor(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() ^ other.bits()),

type Output = PageFlags

The resulting type after applying the ^ operator.

impl BitXorAssign for PageFlags

fn bitxor_assign(&mut self, other: Self)

Performs the ^= operation. Read more

impl BitXorSpecImpl for PageFlags

open spec fn obeys_bitxor_spec() -> bool

{ true }

open spec fn bitxor_req(self, rhs: Self) -> bool

{ true }

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

{ self.symmetric_difference(rhs) }

impl Clone for PageFlags

exec fn clone(&self) -> r : Self

returns

self,

1.0.0 (const: unstable) · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

impl Debug for PageFlags

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

impl Default for PageFlags

exec fn default() -> r : Self

ensures

r.bits() == 0,

r.flags_spec() == Self::flags_from_bits(0),

returns

Self::empty(),

impl Not for PageFlags

exec fn not(self) -> r : Self

ensures

r.bits() == (!self.bits() & PageFlags::all().bits()),

type Output = PageFlags

The resulting type after applying the ! operator.

impl NotSpecImpl for PageFlags

open spec fn obeys_not_spec() -> bool

{ true }

open spec fn not_req(self) -> bool

{ true }

closed spec fn not_spec(self) -> Self::Output

impl PartialEq for PageFlags

exec fn eq(&self, other: &Self) -> r : bool

ensures

r == (self.bits() == other.bits()),

1.0.0 (const: unstable) · Source§

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

exec fn sub(self, other: Self) -> r : Self

ensures

r.bits() == (self.bits() & !other.bits()),

type Output = PageFlags

The resulting type after applying the - operator.

impl SubAssign for PageFlags

fn sub_assign(&mut self, other: Self)

Performs the -= operation. Read more

impl SubSpecImpl for PageFlags

open spec fn obeys_sub_spec() -> bool

{ true }

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

{ true }

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

{ self.difference(rhs) }

impl View for PageFlags

open spec fn view(&self) -> Self::V

{ Self::flags_from_bits(self.bits()) }

type V = Set<__ghostPageFlags>

impl Copy for PageFlags

impl Eq for PageFlags

Auto Trait Implementations§

impl Freeze for PageFlags

impl RefUnwindSafe for PageFlags

impl Send for PageFlags

impl Sync for PageFlags

impl Unpin for PageFlags

impl UnsafeUnpin for PageFlags

impl UnwindSafe for PageFlags

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<Rhs, VERUS_SPEC__A> BitAndAssignSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitAndAssign<Rhs> + ?Sized,

fn obeys_bitand_assign_spec() -> bool

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

fn bitand_assign_spec(&self, rhs: Rhs) -> &VERUS_SPEC__A

impl<Rhs, VERUS_SPEC__A> BitAndSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitAnd<Rhs> + ?Sized,

fn obeys_bitand_spec() -> bool

fn bitand_req(self, rhs: Rhs) -> bool

fn bitand_spec(self, rhs: Rhs) -> <VERUS_SPEC__A as BitAnd<Rhs>>::Output

impl<Rhs, VERUS_SPEC__A> BitOrAssignSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitOrAssign<Rhs> + ?Sized,

fn obeys_bitor_assign_spec() -> bool

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

fn bitor_assign_spec(&self, rhs: Rhs) -> &VERUS_SPEC__A

impl<Rhs, VERUS_SPEC__A> BitOrSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitOr<Rhs> + ?Sized,

fn obeys_bitor_spec() -> bool

fn bitor_req(self, rhs: Rhs) -> bool

fn bitor_spec(self, rhs: Rhs) -> <VERUS_SPEC__A as BitOr<Rhs>>::Output

impl<Rhs, VERUS_SPEC__A> BitXorAssignSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitXorAssign<Rhs> + ?Sized,

fn obeys_bitxor_assign_spec() -> bool

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

fn bitxor_assign_spec(&self, rhs: Rhs) -> &VERUS_SPEC__A

impl<Rhs, VERUS_SPEC__A> BitXorSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: BitXor<Rhs> + ?Sized,

fn obeys_bitxor_spec() -> bool

fn bitxor_req(self, rhs: Rhs) -> bool

fn bitxor_spec(self, rhs: Rhs) -> <VERUS_SPEC__A as BitXor<Rhs>>::Output

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<VERUS_SPEC__A> NotSpec for VERUS_SPEC__A
where VERUS_SPEC__A: Not + ?Sized,

fn obeys_not_spec() -> bool

fn not_req(self) -> bool

fn not_spec(self) -> <VERUS_SPEC__A as Not>::Output

impl<A, Rhs> PartialEqIs<Rhs> for A
where A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

fn is_eq(&self, other: &Rhs) -> bool

fn is_ne(&self, other: &Rhs) -> bool

impl<Rhs, VERUS_SPEC__A> PartialEqSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

fn obeys_eq_spec() -> bool

fn eq_spec(&self, other: &Rhs) -> bool

impl<Rhs, VERUS_SPEC__A> SubAssignSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: SubAssign<Rhs> + ?Sized,

fn obeys_sub_assign_spec() -> bool

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

fn sub_assign_spec(&self, rhs: Rhs) -> &VERUS_SPEC__A

impl<Rhs, VERUS_SPEC__A> SubSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: Sub<Rhs> + ?Sized,

fn obeys_sub_spec() -> bool

fn sub_req(self, rhs: Rhs) -> bool

fn sub_spec(self, rhs: Rhs) -> <VERUS_SPEC__A as Sub<Rhs>>::Output

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

impl<T, U> TryFrom for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto for T
where U: TryFrom<T>,

type Error = >::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, >::Error>

impl<A> SpecEq<&A> for A
where A: ?Sized,

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

impl<A> SpecEq<A> for A
where A: ?Sized,

impl<A> SpecEq<Ghost<A>> for A