Skip to main content

DeepView

vstd::view

Trait DeepView 

Source 
pub trait DeepView {
    type V;

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

Source§

type V = bool

Source§

fn deep_view(&self) -> bool

Source§

impl DeepView for char

Source§

type V = char

Source§

fn deep_view(&self) -> char

Source§

impl DeepView for i8

Source§

type V = i8

Source§

fn deep_view(&self) -> i8

Source§

impl DeepView for i16

Source§

type V = i16

Source§

fn deep_view(&self) -> i16

Source§

impl DeepView for i32

Source§

type V = i32

Source§

fn deep_view(&self) -> i32

Source§

impl DeepView for i64

Source§

type V = i64

Source§

fn deep_view(&self) -> i64

Source§

impl DeepView for i128

Source§

type V = i128

Source§

fn deep_view(&self) -> i128

Source§

impl DeepView for isize

Source§

type V = isize

Source§

fn deep_view(&self) -> isize

Source§

impl DeepView for str

Available on non-verus_verify_core only.
Source§

open spec fn deep_view(&self) -> Seq<char>

{ self.view() }
Source§

type V = Seq<char>

Source§

impl DeepView for u8

Source§

type V = u8

Source§

fn deep_view(&self) -> u8

Source§

impl DeepView for u16

Source§

type V = u16

Source§

fn deep_view(&self) -> u16

Source§

impl DeepView for u32

Source§

type V = u32

Source§

fn deep_view(&self) -> u32

Source§

impl DeepView for u64

Source§

type V = u64

Source§

fn deep_view(&self) -> u64

Source§

impl DeepView for u128

Source§

type V = u128

Source§

fn deep_view(&self) -> u128

Source§

impl DeepView for ()

Source§

type V = ()

Source§

fn deep_view(&self)

Source§

impl DeepView for usize

Source§

type V = usize

Source§

fn deep_view(&self) -> usize

Source§

impl DeepView for String

Available on crate feature alloc and non-verus_verify_core only.
Source§

open spec fn deep_view(&self) -> Seq<char>

{ self.view() }
Source§

type V = Seq<char>

Source§

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

Available on crate feature alloc only.
Source§

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

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

type V = Seq<char>

Source§

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

Available on crate feature alloc only.
Source§

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

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

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

Source§

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

Available on crate feature alloc only.
Source§

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

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

type V = <T as DeepView>::V

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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)

Source§

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)

Source§

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<A0: DeepView, A1: DeepView, A2: DeepView, A3: DeepView, A4: DeepView> DeepView for (A0, A1, A2, A3, A4)

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

fn deep_view(&self) -> (A0::V, A1::V, A2::V, A3::V, A4::V, A5::V, A6::V, A7::V)

Source§

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

Source§

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

Source§

fn deep_view( &self, ) -> (A0::V, A1::V, A2::V, A3::V, A4::V, A5::V, A6::V, A7::V, A8::V)

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

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

type V = <A as DeepView>::V

Source§

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

Available on crate feature alloc only.
Source§

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

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

type V = <A as DeepView>::V

Source§

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

Available on crate feature alloc only.
Source§

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

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

type V = <A as DeepView>::V

Source§

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

Available on crate feature alloc only.
Source§

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

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

type V = <A as DeepView>::V

Source§

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

Source§

open spec fn deep_view(&self) -> Set<Key::V>

{ self@.map(|x: Key| x.deep_view()) }
Source§

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

Source§

impl<Key: DeepView, S, A: Allocator> DeepView for HashSet<Key, S, A>

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

open spec fn deep_view(&self) -> Set<Key::V>

{ self@.map(|x: Key| x.deep_view()) }
Source§

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

Source§

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

Source§

open spec fn deep_view(&self) -> Map<Key::V, Value::V>

{ btree_map_deep_view_impl(*self) }
Source§

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

Source§

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

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

open spec fn deep_view(&self) -> Map<Key::V, Value::V>

{ crate::std_specs::hash::hash_map_deep_view_impl(*self) }
Source§

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

Source§

impl<T: DeepView> DeepView for Option<T>

Source§

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

{
    match self {
        Some(t) => Some(t.deep_view()),
        None => None,
    }
}
Source§

type V = Option<<T 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())
}
Source§

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

Source§

impl<T: DeepView, A: Allocator> DeepView for VecDeque<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())
}
Source§

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

Source§

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

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

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

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

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())
}
Source§

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

Implementors§

Source§

impl<T: DeepView + Hash + Eq> DeepView for ExecMultiset<T>

Implementations for shared traits

Source§

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