Skip to main content

View

creusot_std::model

Trait View

pub trait View {
    type ViewTy;

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

Expand description

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(opaque) ^⚠

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 View for String

Available on crate feature std only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

type ViewTy = Seq<char>

impl View for Duration

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

ensures

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

type ViewTy = Int

impl View for Instant

Available on crate feature std only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

ensures

result >= 0

type ViewTy = Int

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

fn view(self) -> Self::ViewTy

logic(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

logic(opaque) ^⚠

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

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

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

type ViewTy = &'a [T]

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

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

logic(opaque) ^⚠

type ViewTy = Option<&'a T>

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

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

logic(opaque) ^⚠

type ViewTy = Option<&'a mut T>

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

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

type ViewTy = &'a [T]

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

fn view(self) -> Self::ViewTy

logic(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

logic(opaque) ^⚠

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

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

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

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

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

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

fn view(self) -> Option<I>

logic(opaque) ^⚠

type ViewTy = Option<I>

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

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

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

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

impl<T> View for [T]

fn view(self) -> Self::ViewTy

logic ^⚠

type ViewTy = Seq<T>

impl<T> View for Once<T>

fn view(self) -> Option<T>

logic(opaque) ^⚠

type ViewTy = Option<T>

impl<T> View for Repeat<T>

fn view(self) -> T

logic(opaque) ^⚠

type ViewTy = T

impl<T> View for IntoIter<T>

fn view(self) -> Option<T>

logic(opaque) ^⚠

type ViewTy = Option<T>

impl<T> View for MaybeUninit<T>

fn view(self) -> Option<T>

logic(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>

logic(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

logic(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>

logic(opaque) ^⚠

ensures

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

type ViewTy = Seq<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(opaque) ^⚠

type ViewTy = Seq<T>

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(opaque) ^⚠

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

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

Available on crate feature nightly only.

fn view(self) -> Self::ViewTy

logic(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

logic(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

logic(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

logic(opaque) ^⚠

type ViewTy = Box<T>

Implementors§

impl View for Tokens<'_>

type ViewTy = Set<Namespace>

impl View for PeanoInt

type ViewTy = u64

impl<C: ?Sized + Container<Value: Sized>> View for Perm<C>

type ViewTy = <C as Container>::Value

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

type ViewTy = R

impl<R: UnitRA> View for Authority<R>

type ViewTy = R

impl<R: UnitRA> View for Fragment<R>

type ViewTy = R

impl<T> View for SeqIter<T>

type ViewTy = Seq<T>

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

type ViewTy = Seq<T>

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

type ViewTy = Mapping<T, bool>