vstd
In vstd::
slice
Structs
ExIter
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_
_verus_external_fn_specification_7__60__32__91_T_93__32__62__32__58__58__32_iter
axiom_slice_get_usize
axiom_spec_len
group_slice_axioms
slice_index_get
slice_subrange
slice_to_vec
spec_slice_get
spec_slice_len
vstd
::
slice
Function
slice_to_vec
Copy item path
Settings
Help
Summary
Source
pub
exec
fn slice_to_vec<T:
Copy
>(slice: &
[T]
) ->
out :
Vec
<T>
Expand description
ensures
out@ == slice@,