vstd
In vstd::
std_
specs::
vec
Structs
ExVec
Traits
VecAdditionalSpecFns
Functions
_verus_external_fn_specification_233_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_len
_verus_external_fn_specification_234_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_new
_verus_external_fn_specification_235_Vec_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_236_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve
_verus_external_fn_specification_237_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push
_verus_external_fn_specification_238_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop
_verus_external_fn_specification_239_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_append
_verus_external_fn_specification_240_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_extend__from__slice
_verus_external_fn_specification_241_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_insert
_verus_external_fn_specification_242_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_remove
_verus_external_fn_specification_243_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_clear
_verus_external_fn_specification_244_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_as__slice
_verus_external_fn_specification_245_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_split__off
_verus_external_fn_specification_246__60__32_Vec_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
_verus_external_fn_specification_247_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate
_verus_external_fn_specification_248_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize
axiom_spec_len
axiom_vec_index_decreases
group_vec_axioms
spec_vec_len
vec_clone_deep_view_proof
vec_clone_trigger
vec_index
?
Settings
Function
vstd
::
std_specs
::
vec
::
vec_clone_trigger
Copy item path
source
·
[
−
]
pub
open spec
fn vec_clone_trigger<T, A:
Allocator
>(v1:
Vec
<T, A>, v2:
Vec
<T, A>) ->
bool
Expand description
{
true
}