Trait Objective 

pub auto trait Objective { }

An assertion whose meaning is independent of this thread’s view.

Since Objective refers to ghost objects whose memory is objective, Rust’s Unique<T> (and therefore Box<T>, Vec<T>, …) are therefore objective.

Implementors

impl Objective for Perm<AtomicBool>

impl Objective for Perm<AtomicI8>

impl Objective for Perm<AtomicI16>

impl Objective for Perm<AtomicI32>

impl Objective for Perm<AtomicI64>

impl Objective for Perm<AtomicIsize>

impl Objective for Perm<AtomicU8>

impl Objective for Perm<AtomicU16>

impl Objective for Perm<AtomicU32>

impl Objective for Perm<AtomicU64>

impl Objective for Perm<AtomicUsize>

impl<T> Objective for Perm<AtomicPtr<T>>

impl<T> Objective for AtView<T>

Auto implementors

impl<C> !Objective for Perm<C>

impl Objective for Namespace

impl Objective for PositiveReal

impl Objective for Real

impl Objective for Id

impl Objective for Int

impl Objective for Nat

impl Objective for PeanoInt

impl Objective for PtrDeepModel

impl Objective for AtomicBool

impl Objective for AtomicI8

impl Objective for AtomicI16

impl Objective for AtomicI32

impl Objective for AtomicI64

impl Objective for AtomicIsize

impl Objective for AtomicU8

impl Objective for AtomicU16

impl Objective for AtomicU32

impl Objective for AtomicU64

impl Objective for AtomicUsize

impl Objective for SyncView

impl<'a> Objective for Tokens<'a>

impl<'a, T> Objective for PtrLive<'a, T>

where T: Objective,

impl<'scope, 'env> Objective for Scope<'scope, 'env>

impl<A, B> Objective for Mapping<A, B>

where A: ?Sized,

impl<I, F> Objective for MapInv<I, F>

where I: Objective, F: Objective, <I as Iterator>::Item: Objective,

impl<K, V> Objective for FMap<K, V>

where K: Objective, V: Objective,

impl<K, V> Objective for creusot_std::logic::fmap::Iter<K, V>

where K: Objective, V: Objective,

impl<K, V> Objective for FMapInsertLocalUpdate<K, V>

where K: Objective, V: Objective,

impl<R> Objective for Authority<R>

where R: Objective,

impl<R> Objective for Fragment<R>

where R: Objective,

impl<R> Objective for Resource<R>

where R: Objective,

impl<R> Objective for OpLocalUpdate<R>

where R: Objective,

impl<R> Objective for View<R>

where <R as ViewRel>::Frag: Objective, <R as ViewRel>::Auth: Objective,

impl<R> Objective for ViewUpdateInsert<R>

where <R as ViewRel>::Auth: Objective, <R as ViewRel>::Frag: Objective,

impl<R> Objective for ViewUpdateRemove<R>

where <R as ViewRel>::Auth: Objective,

impl<R, Choice> Objective for ViewUpdate<R, Choice>

impl<T> Objective for PermCell<T>

where T: Objective + ?Sized,

impl<T> Objective for PredCell<T>

where T: Objective + ?Sized,

impl<T> Objective for AtomicInvariant<T>

where T: Objective,

impl<T> Objective for AtomicInvariantSC<T>

where T: Objective,

impl<T> Objective for NonAtomicInvariant<T>

where T: Objective,

impl<T> Objective for Ghost<T>

where T: Objective + ?Sized,

impl<T> Objective for Subset<T>

where T: Objective,

impl<T> Objective for Ag<T>

where T: Objective,

impl<T> Objective for AuthViewRel<T>

where T: Objective,

impl<T> Objective for Excl<T>

where T: Objective,

impl<T> Objective for ExclUpdate<T>

where T: Objective,

impl<T> Objective for creusot_std::logic::seq::Iter<T>

where T: Objective,

impl<T> Objective for Seq<T>

where T: Objective,

impl<T> Objective for FSet<T>

where T: Objective,

impl<T> Objective for Set<T>

where T: Objective + ?Sized,

impl<T> Objective for Snapshot<T>

where T: Objective + ?Sized,

impl<T> Objective for AtomicPtr<T>

where T: Objective,

impl<T, C> Objective for LoadCommitter<T, C>

where T: Objective, C: Objective,

impl<T, C> Objective for StoreCommitter<T, C>

where T: Objective, C: Objective,

impl<T, U> Objective for Sum<T, U>

where T: Objective, U: Objective,

impl<U> Objective for AuthUpdate<U>

where U: Objective,

impl<U> Objective for OptionLocalUpdate<U>

where U: Objective,

impl<U> Objective for OptionUpdate<U>

where U: Objective,

impl<U> Objective for SumLocalUpdateL<U>

where U: Objective,

impl<U> Objective for SumLocalUpdateR<U>

where U: Objective,

impl<U> Objective for SumUpdateL<U>

where U: Objective,

impl<U> Objective for SumUpdateR<U>

where U: Objective,