Struct GhostShared
Source pub struct GhostShared<T>();
Expand description
A type for sharing ghost data immutably.
Create a new shared ghost value.
Note that the original value can never be retrieved, which allows this
function to resolve it (in GhostShared’s type invariant).
terminates
ghost
The logical value contained in this GhostShared.
logic ⚠
Access the value of the GhostShared immutably.
terminates
ghost
Performs copy-assignment from
source.
Read more
The resulting type after dereferencing.
logic(open, prophetic)
resolve(self.val()) && inv(self.val())
Immutably borrows from an owned value.
Read more
Mutably borrows from an owned value.
Read more
🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from
self to
dest.
Read more
Returns the argument unchanged.
Calls U::from(self).
That is, this conversion is whatever the implementation of
From<T> for U chooses to do.
🔬This is a nightly-only experimental API. (arbitrary_self_types)
The target type on which the method may be called.
The resulting type after obtaining ownership.
Creates owned data from borrowed data, usually by cloning.
Read more
Uses borrowed data to replace owned data, usually by cloning.
Read more
The type returned in the event of a conversion error.
Performs the conversion.
The type returned in the event of a conversion error.
Performs the conversion.