Struct Id 

pub struct Id(/* private fields */);

A unique id, usable in logic and ghost code

The only properties of this type are:

• there is an infinite number of ids
• You can always generate a fresh id in logic code

Usage

Ids are used in PermCell and resource algebras.

Trait Implementations

impl Clone for Id

fn clone(&self) -> Self

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl Copy for Id

impl DeepModel for Id

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self

type DeepModelTy = Id

impl Eq for Id

impl PartialEq for Id

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

ghost

ensures

result == (*self == *other)

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

ghost

ensures

result != (*self == *other)

impl Plain for Id

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

ghost