Trait InputSlice 

pub trait InputSlice: View<V = Seq<u8>> + DeepView<V = Seq<u8>> {
    // Required method
    proof fn deep_view_eq_view(&self);
}

A byte input whose ordinary and deep views denote the same byte sequence.

Required Methods

proof fn deep_view_eq_view(&self)

ensures

self.deep_view() == self@,

Proves that the two logical views of this input agree.

Implementations on Foreign Types

impl<'input> InputSlice for &'input [u8]

proof fn deep_view_eq_view(&self)

Implementors