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

logic

Implementations on Foreign Types

impl View for char

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for i8

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for i16

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for i32

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for i64

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for i128

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for isize

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for str

fn view(self) -> Self::ViewTy

logic

type ViewTy = Seq<char>

impl View for u8

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for u16

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for u32

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for u64

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for u128

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

impl View for usize

fn view(self) -> Self::ViewTy

logic

type ViewTy = Int

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

type ViewTy = &'a [T]

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

impl<T> View for [T]

fn view(self) -> Self::ViewTy

logic

ensures

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

ensures

result == slice_model(&self)

type ViewTy = Seq<T>

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

fn view(self) -> Self::ViewTy

logic

type ViewTy = T

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

fn view(self) -> Self::ViewTy

logic

type ViewTy = T

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

fn view(self) -> Self::ViewTy

logic

type ViewTy = Seq<T>

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

fn view(self) -> Self::ViewTy

logic

type ViewTy = Seq<T>

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

fn view(self) -> Self::ViewTy

logic

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

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

fn view(self) -> Self::ViewTy

logic

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

impl<T: View + ?Sized> View for &T

fn view(self) -> Self::ViewTy

logic

(*self).view()

type ViewTy = <T as View>::ViewTy

impl<T: View + ?Sized> View for &mut T

fn view(self) -> Self::ViewTy

logic

(*self).view()

type ViewTy = <T as View>::ViewTy

impl<T: ?Sized> View for *const T

fn view(self) -> Int

logic

self.addr_logic()

type ViewTy = Int

impl<T: ?Sized> View for *mut T

fn view(self) -> Int

logic

self.addr_logic()

type ViewTy = Int

Implementors

impl View for PeanoInt

type ViewTy = Int

impl View for String

type ViewTy = Seq<char>

impl View for Duration

type ViewTy = Int

impl View for Instant

type ViewTy = Int

impl<'a, T> View for creusot_contracts::std::option::Iter<'a, T>

type ViewTy = Option<&'a T>

impl<'a, T> View for creusot_contracts::std::option::IterMut<'a, T>

type ViewTy = Option<&'a mut T>

impl<'a, T> View for creusot_contracts::std::slice::Iter<'a, T>

type ViewTy = &'a [T]

impl<'a, T> View for creusot_contracts::std::slice::IterMut<'a, T>

type ViewTy = &'a mut [T]

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

type ViewTy = Option<I>

impl<T> View for PCellOwn<T>

type ViewTy = T

impl<T> View for Once<T>

type ViewTy = Option<T>

impl<T> View for Repeat<T>

type ViewTy = T

impl<T> View for creusot_contracts::std::option::IntoIter<T>

type ViewTy = Option<T>

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

type ViewTy = Seq<T>

impl<T, A: Allocator> View for creusot_contracts::std::vec::IntoIter<T, A>

type ViewTy = Seq<T>

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

type ViewTy = Seq<T>

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

type ViewTy = <T as View>::ViewTy

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

type ViewTy = <T as View>::ViewTy

impl<T: View> View for Ghost<T>

type ViewTy = <T as View>::ViewTy