Skip to main content

View

vest_lib::prelude

Trait View

pub trait View {
    type V;

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

Expand description

Types used in executable code can implement View to provide a mathematical abstraction of the type. For example, Vec implements a view method that returns a Seq. For base types like bool and u8, the view V of the type is the type itself. Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.

Required Associated Types§

type V

Required Methods§

fn view(&self) -> Self::V

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types§

impl View for ()

type V = ()

fn view(&self)

impl View for DefaultHasher

type V = Seq<Seq<u8>>

fn view(&self) -> Seq<Seq<u8>>

impl View for String

Available on crate feature alloc and non-verus_verify_core only.

type V = Seq<char>

fn view(&self) -> Seq<char>

impl View for bool

type V = bool

fn view(&self) -> bool

impl View for char

type V = char

fn view(&self) -> char

impl View for i8

type V = i8

fn view(&self) -> i8

impl View for i16

type V = i16

fn view(&self) -> i16

impl View for i32

type V = i32

fn view(&self) -> i32

impl View for i64

type V = i64

fn view(&self) -> i64

impl View for i128

type V = i128

fn view(&self) -> i128

impl View for isize

type V = isize

fn view(&self) -> isize

impl View for str

Available on non-verus_verify_core only.

type V = Seq<char>

fn view(&self) -> Seq<char>

impl View for u8

type V = u8

fn view(&self) -> u8

impl View for u16

type V = u16

fn view(&self) -> u16

impl View for u32

type V = u32

fn view(&self) -> u32

impl View for u64

type V = u64

fn view(&self) -> u64

impl View for u128

type V = u128

fn view(&self) -> u128

impl View for usize

type V = usize

fn view(&self) -> usize

impl<'a, Key, Value, A> View for CursorMut<'a, Key, Value, A>

type V = CursorMutModel<Key, Value>

fn view(&self) -> CursorMutModel<Key, Value>

impl<'a, T> View for Cow<'a, T>
where T: View + Clone,

Available on crate feature alloc only.

type V = <T as View>::V

fn view(&self) -> <Cow<'a, T> as View>::V

impl<'a, T> View for Cow<'a, [T]>
where T: View + Clone,

Available on crate feature alloc only.

type V = Seq<T>

fn view(&self) -> <Cow<'a, [T]> as View>::V

impl<'a> View for Cow<'a, str>

Available on crate feature alloc only.

type V = Seq<char>

fn view(&self) -> <Cow<'a, str> as View>::V

impl<A0, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11> View for (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View, A7: View, A8: View, A9: View, A10: View, A11: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V, <A10 as View>::V, <A11 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V, <A10 as View>::V, <A11 as View>::V)

impl<A0, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10> View for (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View, A7: View, A8: View, A9: View, A10: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V, <A10 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V, <A10 as View>::V)

impl<A0, A1, A2, A3, A4, A5, A6, A7, A8, A9> View for (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View, A7: View, A8: View, A9: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V, <A9 as View>::V)

impl<A0, A1, A2, A3, A4, A5, A6, A7, A8> View for (A0, A1, A2, A3, A4, A5, A6, A7, A8)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View, A7: View, A8: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V, <A8 as View>::V)

impl<A0, A1, A2, A3, A4, A5, A6, A7> View for (A0, A1, A2, A3, A4, A5, A6, A7)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View, A7: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V, <A7 as View>::V)

impl<A0, A1, A2, A3, A4, A5, A6> View for (A0, A1, A2, A3, A4, A5, A6)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View, A6: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V, <A6 as View>::V)

impl<A0, A1, A2, A3, A4, A5> View for (A0, A1, A2, A3, A4, A5)
where A0: View, A1: View, A2: View, A3: View, A4: View, A5: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V, <A5 as View>::V)

impl<A0, A1, A2, A3, A4> View for (A0, A1, A2, A3, A4)
where A0: View, A1: View, A2: View, A3: View, A4: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V, <A4 as View>::V)

impl<A0, A1, A2, A3> View for (A0, A1, A2, A3)
where A0: View, A1: View, A2: View, A3: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V)

fn view( &self, ) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V)

impl<A0, A1, A2> View for (A0, A1, A2)
where A0: View, A1: View, A2: View,

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V)

fn view(&self) -> (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V)

impl<A0, A1> View for (A0, A1)
where A0: View, A1: View,

type V = (<A0 as View>::V, <A1 as View>::V)

fn view(&self) -> (<A0 as View>::V, <A1 as View>::V)

impl<A0> View for (A0,)
where A0: View,

type V = (<A0 as View>::V,)

fn view(&self) -> (<A0 as View>::V,)

impl<A> View for &A
where A: View + ?Sized,

type V = <A as View>::V

fn view(&self) -> <A as View>::V

impl<A> View for Arc<A>
where A: View,

Available on crate feature alloc only.

type V = <A as View>::V

fn view(&self) -> <A as View>::V

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

Available on crate feature alloc only.

type V = <A as View>::V

fn view(&self) -> <A as View>::V

impl<A> View for Rc<A>
where A: View,

Available on crate feature alloc only.

type V = <A as View>::V

fn view(&self) -> <A as View>::V

impl<Idx> View for RangeInclusive<Idx>

type V = RangeInclusiveView<Idx>

fn view(&self) -> <RangeInclusive<Idx> as View>::V

impl<Key, A> View for BTreeSet<Key, A>
where A: Allocator + Clone,

type V = Set<Key>

fn view(&self) -> Set<Key>

impl<Key, S, A> View for HashSet<Key, S, A>
where A: Allocator,

Available on crate feature alloc and crate feature std and (verus_keep_ghost or crate feature allocator) only.

type V = Set<Key>

fn view(&self) -> Set<Key>

impl<Key, Value, A> View for BTreeMap<Key, Value, A>
where A: Allocator + Clone,

type V = Map<Key, Value>

fn view(&self) -> Map<Key, Value>

impl<Key, Value, S, A> View for HashMap<Key, Value, S, A>
where A: Allocator,

Available on crate feature alloc and crate feature std and (verus_keep_ghost or crate feature allocator) only.

type V = Map<Key, Value>

fn view(&self) -> Map<Key, Value>

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

Available on crate feature alloc and (verus_keep_ghost or crate feature allocator) only.

type V = Seq<T>

fn view(&self) -> Seq<T>

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

type V = Seq<T>

fn view(&self) -> Seq<T>

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

type V = Seq<T>

fn view(&self) -> Seq<T>

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

Available on verus_keep_ghost only.

type V = PtrData<T>

fn view(&self) -> <*const T as View>::V

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

Available on verus_keep_ghost only.

type V = PtrData<T>

fn view(&self) -> <*mut T as View>::V

impl<T> View for ManuallyDrop<T>

type V = T

fn view(&self) -> <ManuallyDrop<T> as View>::V

impl<T> View for NonZero<T>
where T: ZeroablePrimitive,

type V = T

fn view(&self) -> <NonZero<T> as View>::V

impl<T> View for Option<T>

type V = Option<T>

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

impl<T> View for [T]

type V = Seq<T>

fn view(&self) -> Seq<T>

Implementors§

impl View for CheckedU8

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU16

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU32

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU64

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU128

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedUsize

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for OutputSlice<'_>

type V = Seq<u8>

impl View for StringHashSet

type V = Set<Seq<char>>

impl<A: View, B: View> View for Sum<A, B>

type V = Sum<<A as View>::V, <B as View>::V>

impl<Key, Value> View for HashMapWithView<Key, Value>
where Key: View + Eq + Hash,

type V = Map<<Key as View>::V, Value>

impl<Key> View for HashSetWithView<Key>
where Key: View + Eq + Hash,

type V = Set<<Key as View>::V>

impl<T> View for Commit<T>

type V = T

impl<T> View for PointsTo<T>

type V = PointsToData<T>

impl<Value> View for StringHashMap<Value>

type V = Map<Seq<char>, Value>