Skip to main content

SumResource

vstd_extra::resource::ghost_resource::csum

Struct SumResource 

Source 
pub struct SumResource<A, B, const TOTAL: u64 = 2> { /* private fields */ }
Expand description

SumResource is a token that maintains access to a resource of either type A or type B. It can be split into up to TOTAL fractions, one of which have the exclusive right to access the resource, and others shares the knowledge of the resource’s existence and type, but not the ability to access it.

Implementations§

Source§

impl<A, B, const TOTAL: u64> SumResource<A, B, TOTAL>

Source

pub closed spec fn id(self) -> Loc

Returns the unique identifier.

Source

pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL>

The underlying protocol monoid value for this resource.

Source

pub open spec fn is_resource_owner(self) -> bool

{ self.protocol_monoid().is_resource_owner() }

Whether this token has the right to access the underlying resource.

Source

pub open spec fn resource(self) -> Sum<A, B>

{ self.protocol_monoid().resource() }

The resource value, only meaningful if is_resource_owner is true.

Source

pub open spec fn resource_left(self) -> A

{ self.resource()->Left_0 }

The resource value if this token is in the left variant, only meaningful if is_resource_owner is true.

Source

pub open spec fn resource_right(self) -> B

{ self.resource()->Right_0 }

The resource value if this token is in the right variant, only meaningful if is_resource_owner is true.

Source

pub open spec fn is_left(self) -> bool

{ self.protocol_monoid().is_left() }

Whether this token is a Left variant.

Source

pub open spec fn is_right(self) -> bool

{ self.protocol_monoid().is_right() }

Whether this token is a Right variant.

Source

pub open spec fn has_resource(self) -> bool

{
    let p = self.protocol_monoid();
    p.is_resource_owner() && p.has_resource()
}

Whether the resource is currently stored, returns false if this token is not the resource owner.

Source

pub open spec fn has_no_resource(self) -> bool

{
    let p = self.protocol_monoid();
    p.is_resource_owner() && p.has_no_resource()
}

Whether the resource has been taken, returns false if this token is not the resource owner.

Source

pub open spec fn frac(self) -> int

{ self.protocol_monoid().frac() }

The fraction this token represents.

Source

pub open spec fn wf(self) -> bool

{
    &&& 1 <= self.frac() <= TOTAL
    &&& self.protocol_monoid().is_valid()
    &&& self.is_resource_owner() ==> (self.has_resource() <==> !self.has_no_resource())
    &&& (self.is_left() <==> !self.is_right())

}

Type invariant.

Source

pub proof fn alloc_left(tracked a: A) -> tracked res : Self

requires
TOTAL > 0,
ensures
res.is_left(),
res.is_resource_owner(),
res.has_resource(),
res.resource() == Sum::<A, B>::Left(a),
res.frac() == TOTAL,
res.wf(),

Allocates a new SumResource with the resource of type A.

Source

pub proof fn alloc_right(tracked b: B) -> tracked res : Self

requires
TOTAL > 0,
ensures
res.is_right(),
res.is_resource_owner(),
res.has_resource(),
res.resource() == Sum::<A, B>::Right(b),
res.frac() == TOTAL,
res.wf(),

Allocates a new SumResource with the resource of type B.

Source

pub proof fn validate(tracked &self)

ensures
self.wf(),

SumResource satisfies its type invariant.

Source

pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)

requires
old(self).is_left() && old(self).is_right() || other.is_left() && other.is_right()
    || old(self).is_left() && other.is_left() && old(self).is_resource_owner()
        && other.is_resource_owner()
    || old(self).is_right() && other.is_right() && old(self).is_resource_owner()
        && other.is_resource_owner(),
ensures
*old(self) == *final(self),
final(self).id() != other.id(),
final(self).wf(),

Two SumResource tokens can not both be the resource owner unless they have different ids.

Source

pub proof fn validate_with_left(tracked &mut self, tracked other: &Left<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_left(),
!(final(self).is_resource_owner() && other.is_resource_owner()),
final(self).frac() + other.frac() <= TOTAL,
final(self).wf(),

The existence of a Left token with the same id ensures this token is also a Left token.

Source

pub proof fn validate_with_right(tracked &mut self, tracked other: &Right<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_right(),
!(final(self).is_resource_owner() && other.is_resource_owner()),
final(self).frac() + other.frac() <= TOTAL,
final(self).wf(),

The existence of a Right token with the same id ensures this token is also a Right token.

Source

pub proof fn validate_with_one_left_owner( tracked &mut self, tracked other: &OneLeftOwner<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_left(),
!final(self).is_resource_owner(),
final(self).frac() + 1 <= TOTAL,
final(self).wf(),

The existence of a OneLeftOwner token with the same id ensures this token is a Left token that is not the resource owner.

Source

pub proof fn validate_with_one_right_owner( tracked &mut self, tracked other: &OneRightOwner<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_right(),
!final(self).is_resource_owner(),
final(self).frac() + 1 <= TOTAL,
final(self).wf(),

The existence of a OneRightOwner token with the same id ensures this token is a Right token that is not the resource owner.

Source

pub proof fn validate_with_one_left_knowledge( tracked &mut self, tracked other: &OneLeftKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_left(),
final(self).frac() + 1 <= TOTAL,
final(self).wf(),

The existence of a OneLeftKnowledge token with the same id ensures this token is a Left token.

Source

pub proof fn validate_with_one_right_knowledge( tracked &mut self, tracked other: &OneRightKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *final(self),
final(self).is_right(),
final(self).frac() + 1 <= TOTAL,
final(self).wf(),

The existence of a OneRightKnowledge token with the same id ensures this token is a Right token.

Source

pub proof fn tracked_borrow_left(tracked &self) -> tracked res : &A

requires
self.is_left(),
self.is_resource_owner(),
self.has_resource(),
ensures
*res == self.resource_left(),

Borrows the resource of type A.

Source

pub proof fn tracked_borrow_right(tracked &self) -> tracked res : &B

requires
self.is_right(),
self.is_resource_owner(),
self.has_resource(),
ensures
*res == self.resource()->Right_0,

Borrows the resource of type B.

Source

pub proof fn split_left_with_resource(tracked &mut self, n: int) -> tracked res : Left<A, B, TOTAL>

requires
old(self).is_left(),
0 < n < old(self).frac(),
ensures
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!final(self).is_resource_owner(),
res.is_resource_owner() <==> old(self).is_resource_owner(),
res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
res.has_resource() ==> res.resource() == old(self).resource_left(),
final(self).wf(),
res.wf(),

Splits a Left token with the given fraction n, and gives the resource to that Left token if available.

Source

pub proof fn split_left_without_resource(tracked &mut self, n: int) -> tracked res : Left<A, B, TOTAL>

requires
old(self).is_left(),
0 < n < old(self).frac(),
ensures
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!res.is_resource_owner(),
final(self).is_resource_owner() <==> old(self).is_resource_owner(),
final(self).is_resource_owner()
    ==> (final(self).has_resource() <==> old(self).has_resource()),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
final(self).wf(),
res.wf(),

Splits a Left token with the given fraction n, without giving the resource to the Left token.

Source

pub proof fn split_right_with_resource(tracked &mut self, n: int) -> tracked res : Right<A, B, TOTAL>

requires
old(self).is_right(),
0 < n < old(self).frac(),
ensures
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!final(self).is_resource_owner(),
res.is_resource_owner() <==> old(self).is_resource_owner(),
res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
res.has_resource() ==> res.resource() == old(self).resource_right(),
final(self).wf(),
res.wf(),

Splits a Right token with the given fraction n, and gives the resource to that Right token if available.

Source

pub proof fn split_right_without_resource(tracked &mut self, n: int) -> tracked res : Right<A, B, TOTAL>

requires
old(self).is_right(),
0 < n < old(self).frac(),
ensures
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!res.is_resource_owner(),
final(self).is_resource_owner() <==> old(self).is_resource_owner(),
final(self).is_resource_owner()
    ==> (final(self).has_resource() <==> old(self).has_resource()),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
final(self).wf(),
res.wf(),

Splits a Right token with the given fraction n, without giving the resource to the Right token.

Source

pub proof fn split_one_left_owner(tracked &mut self) -> tracked res : OneLeftOwner<A, B, TOTAL>

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).frac() > 1,
ensures
final(self).wf(),
final(self).id() == old(self).id(),
final(self).is_left(),
final(self).frac() + 1 == old(self).frac(),
!final(self).is_resource_owner(),
res.id() == old(self).id(),
res.wf(),
res.has_resource() == old(self).has_resource(),
res.has_resource() ==> res.resource() == old(self).resource_left(),

Splits a OneLeftOwner, giving it the resource.

Source

pub proof fn split_one_right_owner(tracked &mut self) -> tracked res : OneRightOwner<A, B, TOTAL>

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).frac() > 1,
ensures
final(self).wf(),
final(self).id() == old(self).id(),
final(self).is_right(),
final(self).frac() + 1 == old(self).frac(),
!final(self).is_resource_owner(),
res.id() == old(self).id(),
res.wf(),
res.has_resource() == old(self).has_resource(),
res.has_resource() ==> res.resource() == old(self).resource_right(),

Splits a OneRightOwner, giving it the resource.

Source

pub proof fn split_one_left_knowledge(tracked &mut self) -> tracked res : OneLeftKnowledge<A, B, TOTAL>

requires
old(self).is_left(),
old(self).frac() > 1,
ensures
final(self).wf(),
final(self).id() == old(self).id(),
final(self).is_left(),
final(self).frac() + 1 == old(self).frac(),
final(self).is_resource_owner() == old(self).is_resource_owner(),
final(self).has_resource() == old(self).has_resource(),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
res.id() == old(self).id(),
res.wf(),

Splits a OneLeftKnowledge, without giving it the resource.

Source

pub proof fn split_one_right_knowledge(tracked &mut self) -> tracked res : OneRightKnowledge<A, B, TOTAL>

requires
old(self).is_right(),
old(self).frac() > 1,
ensures
final(self).wf(),
final(self).id() == old(self).id(),
final(self).is_right(),
final(self).frac() + 1 == old(self).frac(),
final(self).is_resource_owner() == old(self).is_resource_owner(),
final(self).has_resource() == old(self).has_resource(),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
res.id() == old(self).id(),
res.wf(),

Splits a OneRightKnowledge, without giving it the resource.

Source

pub proof fn take_resource_left(tracked &mut self) -> tracked res : A

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
final(self).is_left(),
res == old(self).resource_left(),
final(self).id() == old(self).id(),
final(self).is_resource_owner(),
final(self).has_no_resource(),
final(self).frac() == old(self).frac(),
final(self).wf(),

Takes the resource out of the token if it is in the left variant.

Source

pub proof fn take_resource_right(tracked &mut self) -> tracked res : B

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
final(self).is_right(),
res == old(self).resource_right(),
final(self).id() == old(self).id(),
final(self).is_resource_owner(),
final(self).has_no_resource(),
final(self).frac() == old(self).frac(),
final(self).wf(),

Takes the resource out of the token if it is in the right variant.

Source

pub proof fn put_resource_left(tracked &mut self, tracked a: A)

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_no_resource(),
ensures
final(self).is_left(),
final(self).has_resource(),
final(self).is_resource_owner(),
final(self).resource_left() == a,
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac(),
final(self).wf(),

Puts a resource of type A back to the token.

Source

pub proof fn put_resource_right(tracked &mut self, tracked b: B)

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_no_resource(),
ensures
final(self).is_right(),
final(self).is_resource_owner(),
final(self).has_resource(),
final(self).resource_right() == b,
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac(),
final(self).wf(),

Puts a resource of type B back to the token.

Source

pub proof fn update_left(tracked &mut self, tracked a: A) -> tracked res : Option<A>

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
final(self).is_left(),
final(self).is_resource_owner(),
final(self).has_resource(),
final(self).resource_left() == a,
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac(),
res == Some(old(self).resource_left()),
final(self).wf(),

Updates the resource of type A in the token, when the token is in the left variant and is a resource owner. Returns the old resource if available.

Source

pub proof fn update_right(tracked &mut self, tracked b: B) -> tracked res : Option<B>

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
final(self).is_right(),
final(self).is_resource_owner(),
final(self).has_resource(),
final(self).resource_right() == b,
final(self).id() == old(self).id(),
final(self).frac() == old(self).frac(),
res == Some(old(self).resource_right()),
final(self).wf(),

Updates the resource of type B in the token, when the token is in the right variant and is a resource owner. Returns the old resource if available.

Source

pub proof fn change_to_left(tracked &mut self, tracked a: A) -> tracked res : Option<Sum<A, B>>

requires
old(self).is_resource_owner(),
old(self).frac() == TOTAL,
ensures
final(self).id() == old(self).id(),
final(self).protocol_monoid()
    == SumSP::<A, B, TOTAL>::Left(Some(a), old(self).frac(), true),
final(self).frac() == old(self).frac(),
final(self).is_left(),
final(self).is_resource_owner(),
final(self).has_resource(),
final(self).resource_left() == a,
old(self).has_resource() ==> res == Some(old(self).resource()),
old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
final(self).wf(),

Changes the token to the left invariant with a new resource of type A, and returns the old resource if available.

NOTE: Unlike Self::update_left, this operation can only be done with the full fraction, because there should be no Right tokens to witness the existence of the old resource after the update.

Source

pub proof fn change_to_right(tracked &mut self, tracked b: B) -> tracked res : Option<Sum<A, B>>

requires
old(self).is_resource_owner(),
old(self).frac() == TOTAL,
ensures
final(self).id() == old(self).id(),
final(self).protocol_monoid()
    == SumSP::<A, B, TOTAL>::Right(Some(b), old(self).frac(), true),
final(self).frac() == old(self).frac(),
final(self).is_right(),
final(self).is_resource_owner(),
final(self).has_resource(),
final(self).resource_right() == b,
old(self).has_resource() ==> res == Some(old(self).resource()),
old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
final(self).wf(),

Changes the token to the right invariant with a new resource of type B, and returns the old resource if available.

NOTE: Unlike Self::update_right, this operation can only be done with the full fraction, because there should be no Left tokens to witness the existence of the old resource after the update.

Source

pub proof fn join_left(tracked &mut self, tracked other: Left<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_left(),
final(self).is_resource_owner()
    == (old(self).is_resource_owner() || other.is_resource_owner()),
final(self).has_resource() == (old(self).has_resource() || other.has_resource()),
final(self).has_resource()
    ==> final(self).resource()
        == if old(self).is_resource_owner() {
            old(self).resource()
        } else {
            Sum::Left(other.resource())
        },
final(self).frac() == old(self).frac() + other.frac(),
final(self).wf(),

Joins this token with another Left token with the same id.

Source

pub proof fn join_right(tracked &mut self, tracked other: Right<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_right(),
final(self).is_resource_owner()
    == (old(self).is_resource_owner() || other.is_resource_owner()),
final(self).has_resource() == (old(self).has_resource() || other.has_resource()),
final(self).has_resource()
    ==> final(self).resource()
        == if old(self).is_resource_owner() {
            old(self).resource()
        } else {
            Sum::Right(other.resource())
        },
final(self).frac() == old(self).frac() + other.frac(),
final(self).wf(),

Joins this token with another Right token with the same id.

Source

pub proof fn join_one_left_owner(tracked &mut self, tracked other: OneLeftOwner<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_left(),
final(self).is_resource_owner(),
final(self).has_resource() == other.has_resource(),
final(self).has_resource() ==> final(self).resource_left() == other.resource(),
final(self).frac() == old(self).frac() + 1,
final(self).wf(),

Joins a OneLeftOwner token.

Source

pub proof fn join_one_right_owner(tracked &mut self, tracked other: OneRightOwner<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_right(),
final(self).is_resource_owner(),
final(self).has_resource() == other.has_resource(),
final(self).has_resource() ==> final(self).resource_right() == other.resource(),
final(self).frac() == old(self).frac() + 1,
final(self).wf(),

Joins a OneRightOwner token.

Source

pub proof fn join_one_left_knowledge(tracked &mut self, tracked other: OneLeftKnowledge<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_left(),
final(self).is_resource_owner() == old(self).is_resource_owner(),
final(self).has_resource() == old(self).has_resource(),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
final(self).frac() == old(self).frac() + 1,
final(self).wf(),

Joins a OneLeftKnowledge token.

Source

pub proof fn join_one_right_knowledge( tracked &mut self, tracked other: OneRightKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
final(self).id() == old(self).id(),
final(self).is_right(),
final(self).is_resource_owner() == old(self).is_resource_owner(),
final(self).has_resource() == old(self).has_resource(),
final(self).has_resource() ==> final(self).resource() == old(self).resource(),
final(self).frac() == old(self).frac() + 1,
final(self).wf(),

Joins a OneRightKnowledge token.

Auto Trait Implementations§

§

impl<A, B, const TOTAL: u64> Freeze for SumResource<A, B, TOTAL>

§

impl<A, B, const TOTAL: u64> RefUnwindSafe for SumResource<A, B, TOTAL>
where A: RefUnwindSafe, B: RefUnwindSafe,

§

impl<A, B, const TOTAL: u64> Send for SumResource<A, B, TOTAL>
where A: Send + Sync, B: Send + Sync,

§

impl<A, B, const TOTAL: u64> Sync for SumResource<A, B, TOTAL>
where A: Sync + Send, B: Sync + Send,

§

impl<A, B, const TOTAL: u64> Unpin for SumResource<A, B, TOTAL>
where A: Unpin, B: Unpin,

§

impl<A, B, const TOTAL: u64> UnsafeUnpin for SumResource<A, B, TOTAL>

§

impl<A, B, const TOTAL: u64> UnwindSafe for SumResource<A, B, TOTAL>
where A: UnwindSafe, B: UnwindSafe,

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

§

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

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

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

§

impl<A> SpecEq<Tracked<A>> for A

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

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

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

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