Trait View 

pub trait View {
    type ViewTy;

    // Required method
    fn view(self) -> Self::ViewTy;
}

The view of a type is its logical model as typically used to specify a data structure. It is typically “shallow”, and does not involve the model of other types contained by the datastructure. This kind of model is mostly useful for notation purposes, because this trait is linked to the @ notation of pearlite.

Required Associated Types

type ViewTy

Required Methods

fn view(self) -> Self::ViewTy

Implementations on Foreign Types

impl View for char

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for i8

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for i16

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for i32

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for i64

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for i128

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for isize

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for str

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Seq<char>

impl View for u8

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for u16

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for u32

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for u64

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for u128

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for usize

fn view(self) -> Self::ViewTy

type ViewTy = Int

impl View for String

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Seq<char>

impl View for Duration

fn view(self) -> Self::ViewTy

(opaque)

ensures

result >= 0 && result <= secs_to_nanos(u64::MAX@) + 999_999_999

type ViewTy = Int

impl View for Instant

fn view(self) -> Self::ViewTy

(opaque)

ensures

result >= 0

type ViewTy = Int

impl<'a, K: DeepModel, V> View for Iter<'a, K, V>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FMap<<K as DeepModel>::DeepModelTy, V>

impl<'a, K: DeepModel, V> View for IterMut<'a, K, V>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FMap<<K as DeepModel>::DeepModelTy, &'a mut V>

impl<'a, T> View for Iter<'a, T>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = &'a [T]

impl<'a, T> View for Iter<'a, T>

fn view(self) -> Option<&'a T>

(opaque)

type ViewTy = Option<&'a T>

impl<'a, T> View for IterMut<'a, T>

fn view(self) -> Option<&'a mut T>

(opaque)

type ViewTy = Option<&'a mut T>

impl<'a, T> View for Iter<'a, T>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = &'a [T]

impl<'a, T> View for IterMut<'a, T>

fn view(self) -> Self::ViewTy

(opaque)

ensures

(^result)@.len() == (*result)@.len()

type ViewTy = &'a mut [T]

impl<'a, T: DeepModel> View for Iter<'a, T>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FSet<<T as DeepModel>::DeepModelTy>

impl<'a, T: DeepModel, S> View for Difference<'a, T, S>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FSet<<T as DeepModel>::DeepModelTy>

impl<'a, T: DeepModel, S> View for Intersection<'a, T, S>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FSet<<T as DeepModel>::DeepModelTy>

impl<I: Iterator> View for Fuse<I>

fn view(self) -> Option<I>

(opaque)

type ViewTy = Option<I>

impl<K: DeepModel, V> View for IntoIter<K, V>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FMap<<K as DeepModel>::DeepModelTy, V>

impl<K: DeepModel, V, S> View for HashMap<K, V, S>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FMap<<K as DeepModel>::DeepModelTy, V>

impl<T> View for [T]

fn view(self) -> Self::ViewTy

type ViewTy = Seq<T>

impl<T> View for Once<T>

fn view(self) -> Option<T>

(opaque)

type ViewTy = Option<T>

impl<T> View for Repeat<T>

fn view(self) -> T

(opaque)

type ViewTy = T

impl<T> View for IntoIter<T>

fn view(self) -> Option<T>

(opaque)

type ViewTy = Option<T>

impl<T, A: Allocator> View for VecDeque<T, A>

Available on crate feature nightly only.

fn view(self) -> Seq<T>

(opaque)

ensures

result.len() <= usize::MAX@

type ViewTy = Seq<T>

impl<T, A: Allocator> View for IntoIter<T, A>

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Seq<T>

impl<T, A: Allocator> View for Vec<T, A>

Available on crate feature nightly only.

fn view(self) -> Seq<T>

(opaque)

ensures

result.len() <= usize::MAX@

type ViewTy = Seq<T>

impl<T, const N: usize> View for [T; N]

fn view(self) -> Self::ViewTy

type ViewTy = Seq<T>

impl<T, const N: usize> View for IntoIter<T, N>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Seq<T>

impl<T: DeepModel> View for IntoIter<T>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FSet<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, S> View for HashSet<T, S>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = FSet<<T as DeepModel>::DeepModelTy>

impl<T: View + ?Sized, A: Allocator> View for Box<T, A>

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

(open, inline)

(*self).view()

type ViewTy = <T as View>::ViewTy

impl<T: ?Sized, A: Allocator> View for Rc<T, A>

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Box<T>

impl<T: ?Sized, A: Allocator> View for Arc<T, A>

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Box<T>

Implementors

impl View for Tokens<'_>

type ViewTy = Set<Namespace>

impl View for PeanoInt

type ViewTy = u64

impl<K, V> View for Authority<K, V>

type ViewTy = FMap<K, V>

impl<K, V> View for Fragment<K, V>

type ViewTy = (K, V)

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

type ViewTy = Mapping<K, Option<V>>

impl<R: RA> View for Resource<R>

type ViewTy = R

impl<T> View for PermCellOwn<T>

type ViewTy = T

impl<T> View for SeqIter<T>

type ViewTy = Seq<T>

impl<T> View for SeqIterRef<'_, T>

type ViewTy = Seq<T>

impl<T: InhabitedInvariant> View for Subset<T>

type ViewTy = T

impl<T: ?Sized> View for PredCell<T>

type ViewTy = Mapping<T, bool>