Trait vstd::view::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

Trait vstd::view::ViewCopy item path

Required Associated Types§

type V

Required Methods§

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

Implementations on Foreign Types§

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

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

type V = 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 ()

type V = ()

fn view(&self)

impl View for usize

type V = usize

fn view(&self) -> usize

impl View for String

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

type V = Seq<char>

impl View for DefaultHasher

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

type V = Seq<Seq<u8>>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type V = <A as View>::V

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

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

type V = <A as View>::V

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

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

Trait vstd::view::View

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

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