Struct Tracked 

pub struct Tracked<A> { /* private fields */ }

Implementations

impl<A> Tracked<A>

pub fn view(self) -> A

pub const fn new(_a: A) -> Tracked<A>

pub const fn get(self) -> A

pub fn borrow(&self) -> &A

pub fn borrow_mut(&mut self) -> &mut A

Trait Implementations

impl<A> Clone for Tracked<A>

where A: Copy,

fn clone(&self) -> Tracked<A>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<A> Copy for Tracked<A>

where A: Copy,

impl<A> Debug for Tracked<A>

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

Formats the value using the given formatter.

impl<A> Deref for Tracked<A>

Available on verus_keep_ghost only.

Dereferencing a Tracked<A> returns a reference to a tracked-mode location.

Note: This special behavior requires support from Verus, and this trait impl cannot be used generically.

type Target = A

The resulting type after dereferencing.

fn deref(&self) -> &<Tracked<A> as Deref>::Target

Dereferences the value.

impl<A> DerefMut for Tracked<A>

Available on verus_keep_ghost only.

Dereferencing a Tracked<A> returns a reference to a tracked-mode location.

Note: This special behavior requires support from Verus, and this trait impl cannot be used generically.

fn deref_mut(&mut self) -> &mut <Tracked<A> as Deref>::Target

Mutably dereferences the value.

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

Available on verus_keep_ghost only.