Struct SyncView 

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

↑V

Implementations

impl SyncView

pub fn new() -> Ghost<Self>

terminates

ghost

Trait Implementations

impl Clone for SyncView

fn clone(&self) -> Self

ensures

result == *self

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

Performs copy-assignment from source.

impl OrdLogic for SyncView

fn cmp_log(self, _: Self) -> Ordering

logic(opaque)

fn cmp_le_log(x: Self, y: Self)

logic(law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

fn le_log(self, o: Self) -> bool

The logical <= operation.

fn lt_log(self, o: Self) -> bool

The logical < operation.

fn ge_log(self, o: Self) -> bool

The logical >= operation.

fn gt_log(self, o: Self) -> bool

The logical > operation.

impl Copy for SyncView