vstd
In vstd::
slice
Traits
ExSliceIndex
SliceAdditionalExecFns
SliceAdditionalSpecFns
Functions
_verus_external_fn_specification_5__60__32__91_T_93__32__62__32__58__58__32_len
_verus_external_fn_specification_6__60__32__91_T_93__32__62__32__58__58__32_get_32__58__58__32__60__32_I_32__62_
axiom_slice_get_usize
axiom_spec_len
group_slice_axioms
slice_index_get
slice_subrange
slice_to_vec
spec_slice_get
spec_slice_len
?
Settings
Function
vstd
::
slice
::
slice_to_vec
Copy item path
source
·
[
−
]
pub
exec
fn slice_to_vec<T:
Copy
>(slice: &
[T]
) ->
out :
Vec
<T>
Expand description
ensures
@ == @,