Function vstd::std_specs::vec::vec_clone_deep_view_proof

source · 
pub broadcast proof fn vec_clone_deep_view_proof<T: DeepView, A: Allocator>(
    v1: Vec<T, A>,
    v2: Vec<T, A>
)
Expand description
requires
#[trigger] vec_clone_trigger(v1, v2),
v1.deep_view() =~= v2.deep_view(),
ensures
v1.deep_view() == v2.deep_view(),