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.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

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

proof fn deep_view_eq_view(&self)

Implementors