vstd
In vstd::
array
Traits
ArrayAdditionalExecFns
ArrayAdditionalSpecFns
Functions
_verus_external_fn_specification_0__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice
array_index_get
array_len_matches_n
array_view
axiom_spec_array_as_slice
axiom_spec_array_fill_for_copy_type
group_array_axioms
lemma_array_index
spec_array_as_slice
spec_array_fill_for_copy_type
?
Settings
Function
vstd
::
array
::
spec_array_as_slice
Copy item path
source
·
[
−
]
pub
uninterp
fn spec_array_as_slice<T, const N:
usize
>(ar: &
[T; N]
) ->
out :
&
[T]
Expand description