vstd::view

Trait View

Source
pub trait View {
    type V;

    // Required method
    spec 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§

Source

type V

Required Methods§

Source

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

Implementations on Foreign Types§

Source§

impl View for bool

Source§

type V = bool

Source§

fn view(&self) -> bool

Source§

impl View for char

Source§

type V = char

Source§

fn view(&self) -> char

Source§

impl View for i8

Source§

type V = i8

Source§

fn view(&self) -> i8

Source§

impl View for i16

Source§

type V = i16

Source§

fn view(&self) -> i16

Source§

impl View for i32

Source§

type V = i32

Source§

fn view(&self) -> i32

Source§

impl View for i64

Source§

type V = i64

Source§

fn view(&self) -> i64

Source§

impl View for i128

Source§

type V = i128

Source§

fn view(&self) -> i128

Source§

impl View for isize

Source§

type V = isize

Source§

fn view(&self) -> isize

Source§

impl View for str

Source§

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

Source§

type V = Seq<char>

Source§

impl View for u8

Source§

type V = u8

Source§

fn view(&self) -> u8

Source§

impl View for u16

Source§

type V = u16

Source§

fn view(&self) -> u16

Source§

impl View for u32

Source§

type V = u32

Source§

fn view(&self) -> u32

Source§

impl View for u64

Source§

type V = u64

Source§

fn view(&self) -> u64

Source§

impl View for u128

Source§

type V = u128

Source§

fn view(&self) -> u128

Source§

impl View for ()

Source§

type V = ()

Source§

fn view(&self)

Source§

impl View for usize

Source§

type V = usize

Source§

fn view(&self) -> usize

Source§

impl View for String

Source§

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

Source§

type V = Seq<char>

Source§

impl View for DefaultHasher

Source§

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

Source§

type V = Seq<Seq<u8>>

Source§

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

Source§

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

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}
Source§

type V = Seq<char>

Source§

impl<'a> View for Chars<'a>

Source§

uninterp fn view(&self) -> (int, Seq<char>)

Source§

type V = (int, Seq<char>)

Source§

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

Source§

uninterp fn view(self: &Iter<'a, T>) -> (int, Seq<T>)

Source§

type V = (int, Seq<T>)

Source§

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

Source§

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

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}
Source§

type V = Seq<T>

Source§

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

Source§

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

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}
Source§

type V = <T as View>::V

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

open spec fn view(&self) -> A::V

{ (**self).view() }
Source§

type V = <A as View>::V

Source§

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

Source§

open spec fn view(&self) -> A::V

{ (**self).view() }
Source§

type V = <A as View>::V

Source§

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

Source§

open spec fn view(&self) -> A::V

{ (**self).view() }
Source§

type V = <A as View>::V

Source§

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

Source§

open spec fn view(&self) -> A::V

{ (**self).view() }
Source§

type V = <A as View>::V

Source§

impl<Key, S> View for HashSet<Key, S>

Source§

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

Source§

type V = Set<Key>

Source§

impl<Key, Value, S> View for HashMap<Key, Value, S>

Source§

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

Source§

type V = Map<Key, Value>

Source§

impl<T> View for Option<T>

Source§

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

{ *self }
Source§

type V = Option<T>

Source§

impl<T> View for [T]

Source§

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

Source§

type V = Seq<T>

Source§

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

Source§

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

Source§

type V = Seq<T>

Source§

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

Source§

uninterp fn view(self: &IntoIter<T, A>) -> (int, Seq<T>)

Source§

type V = (int, Seq<T>)

Source§

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

Source§

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

Source§

type V = Seq<T>

Source§

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

Source§

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

{ array_view(*self) }
Source§

type V = Seq<T>

Source§

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

Source§

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

{ (*self as *mut T).view() }
Source§

type V = PtrData

Source§

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

Source§

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

Source§

type V = PtrData

Implementors§

Source§

impl View for CheckedU8

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

Source§

type V = nat

Source§

impl View for CheckedU16

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

Source§

type V = nat

Source§

impl View for CheckedU32

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

Source§

type V = nat

Source§

impl View for CheckedU64

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

Source§

type V = nat

Source§

impl View for CheckedU128

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

Source§

type V = nat

Source§

impl View for CheckedUsize

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

Source§

type V = nat

Source§

impl View for StringHashSet

Source§

impl<'a> View for CharsGhostIterator<'a>

Source§

impl<'a, Key> View for vstd::std_specs::hash::IterGhostIterator<'a, Key>

Source§

type V = Seq<Key>

Source§

impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value>

Source§

type V = Seq<Key>

Source§

impl<'a, Key, Value> View for ValuesGhostIterator<'a, Key, Value>

Source§

type V = Seq<Value>

Source§

impl<'a, T> View for vstd::std_specs::vecdeque::IterGhostIterator<'a, T>

Source§

type V = Seq<T>

Source§

impl<A: StepSpec + Step> View for RangeGhostIterator<A>

Source§

type V = Seq<A>

Source§

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

Source§

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

Source§

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

Source§

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

Source§

impl<T> View for PointsTo<T>

Source§

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

Source§

type V = Seq<T>

Source§

impl<Value> View for StringHashMap<Value>

Source§

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