vstd
In vstd::
std_
specs::
vecdeque
Structs
ExIter
ExVecDeque
IterGhostIterator
Traits
IterAdditionalSpecFns
VecDequeAdditionalSpecFns
Functions
_verus_external_fn_specification_249_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_index
_verus_external_fn_specification_250_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_len
_verus_external_fn_specification_251_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_new
_verus_external_fn_specification_252_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_253_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve
_verus_external_fn_specification_254_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push__back
_verus_external_fn_specification_255_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_push__front
_verus_external_fn_specification_256_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop__back
_verus_external_fn_specification_257_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_pop__front
_verus_external_fn_specification_258_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_append
_verus_external_fn_specification_259_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_insert
_verus_external_fn_specification_260_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_remove
_verus_external_fn_specification_261_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_clear
_verus_external_fn_specification_262_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_split__off
_verus_external_fn_specification_263__60__32_VecDeque_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
_verus_external_fn_specification_264_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate
_verus_external_fn_specification_265_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize
_verus_external_fn_specification_266_Iter_32__58__58__32__60__32__39_a_44__32_T_32__62__32__58__58__32_next
_verus_external_fn_specification_267_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_iter
axiom_spec_iter
axiom_spec_len
axiom_vec_dequeue_index_decreases
group_vec_dequeue_axioms
spec_iter
spec_vec_dequeue_len
vec_dequeue_clone_trigger
?
Settings
Function
vstd
::
std_specs
::
vecdeque
::
spec_vec_dequeue_len
Copy item path
source
·
[
−
]
pub
uninterp
fn spec_vec_dequeue_len<T, A:
Allocator
>(v: &
VecDeque
<T, A>) ->
usize
Expand description