Trait vstd::view::DeepView

source · 
pub trait DeepView {
    type V;

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

Required Associated Types§

source

type V

Required Methods§

source

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

Implementations on Foreign Types§

source§

impl DeepView for bool

§

type V = bool

source§

fn deep_view(&self) -> bool

source§

impl DeepView for char

§

type V = char

source§

fn deep_view(&self) -> char

source§

impl DeepView for i8

§

type V = i8

source§

fn deep_view(&self) -> i8

source§

impl DeepView for i16

§

type V = i16

source§

fn deep_view(&self) -> i16

source§

impl DeepView for i32

§

type V = i32

source§

fn deep_view(&self) -> i32

source§

impl DeepView for i64

§

type V = i64

source§

fn deep_view(&self) -> i64

source§

impl DeepView for i128

§

type V = i128

source§

fn deep_view(&self) -> i128

source§

impl DeepView for isize

§

type V = isize

source§

fn deep_view(&self) -> isize

source§

impl DeepView for u8

§

type V = u8

source§

fn deep_view(&self) -> u8

source§

impl DeepView for u16

§

type V = u16

source§

fn deep_view(&self) -> u16

source§

impl DeepView for u32

§

type V = u32

source§

fn deep_view(&self) -> u32

source§

impl DeepView for u64

§

type V = u64

source§

fn deep_view(&self) -> u64

source§

impl DeepView for u128

§

type V = u128

source§

fn deep_view(&self) -> u128

source§

impl DeepView for ()

§

type V = ()

source§

fn deep_view(&self)

source§

impl DeepView for usize

§

type V = usize

source§

fn deep_view(&self) -> usize

source§

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

§

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

source§

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

source§

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

§

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

source§

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

source§

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

§

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

source§

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

source§

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

§

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

source§

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

source§

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

source§

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

{ (**self).deep_view() }
§

type V = <A as DeepView>::V

source§

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

source§

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

{ (**self).deep_view() }
§

type V = <A as DeepView>::V

source§

impl<A: DeepView> DeepView for Rc<A>

source§

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

{ (**self).deep_view() }
§

type V = <A as DeepView>::V

source§

impl<A: DeepView> DeepView for Arc<A>

source§

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

{ (**self).deep_view() }
§

type V = <A as DeepView>::V

source§

impl<T: DeepView> DeepView for [T]

source§

open spec fn deep_view(&self) -> Seq<T::V>

{
    let v = self.view();
    Seq::new(v.len(), |i: int| v[i].deep_view())
}
§

type V = Seq<<T as DeepView>::V>

source§

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

source§

open spec fn deep_view(&self) -> Seq<T::V>

{
    let v = self.view();
    Seq::new(v.len(), |i: int| v[i].deep_view())
}
§

type V = Seq<<T as DeepView>::V>

source§

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

source§

open spec fn deep_view(&self) -> Seq<T::V>

{
    let v = self.view();
    Seq::new(v.len(), |i: int| v[i].deep_view())
}
§

type V = Seq<<T as DeepView>::V>

Implementors§