Struct Snapshot 

pub struct Snapshot<T: ?Sized>(/* private fields */);

A copyable snapshot, usable in pearlite.

The Snapshot type contains the logical value of some data, in a purely immutable way. It is zero sized.

Creating a snapshot does not move the ownership of a value.

Pearlite syntax

In executable code, you may create a snapshot with the snapshot! macro. Inside this macro, you may write pearlite code; this code will not run during the normal execution of the program.

Example

let x: Snapshot<Int> = snapshot!(1);
let m: Snapshot<Mapping<Int, Int>> = snapshot!(|x| x + 1);

Implementations

impl<T> Snapshot<T>

pub fn into_ghost(self) -> Ghost<T>

where T: Plain,

Extract a plain value from a snapshot in ghost code.

Trait Implementations

impl<T: ?Sized> Clone for Snapshot<T>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: ?Sized + Fin> Fin for Snapshot<T>

type Target = <T as Fin>::Target

impl<R: RA, Choice> Update<R> for Snapshot<Mapping<Choice, R>>

type Choice = Choice

impl<R: RA> Update<R> for Snapshot<R>

type Choice = ()

impl<T: ?Sized> Copy for Snapshot<T>

impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)>