Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 956_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 957_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 958__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ default_ 32__ 58__ 58__ 32_ Default_ 32__ 62__ 32__ 58__ 58__ 32_ default - _verus_
external_ ⚠fn_ specification_ 959_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ new__ in - _verus_
external_ ⚠fn_ specification_ 960_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 961_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ in - _verus_
external_ ⚠fn_ specification_ 962_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 963_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ try__ reserve - _verus_
external_ ⚠fn_ specification_ 964_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 965_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 966_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ append - _verus_
external_ ⚠fn_ specification_ 967_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ extend__ from__ slice - _verus_
external_ ⚠fn_ specification_ 968_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 969_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ swap__ remove - _verus_
external_ ⚠fn_ specification_ 970_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 971__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 972_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 973_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 974_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ as__ slice - _verus_
external_ ⚠fn_ specification_ 976__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Deref_ 32__ 62__ 32__ 58__ 58__ 32_ deref - _verus_
external_ ⚠fn_ specification_ 977__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Deref Mut_ 32__ 62__ 32__ 58__ 58__ 32_ deref__ mut - _verus_
external_ ⚠fn_ specification_ 978_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ split__ off - _verus_
external_ ⚠fn_ specification_ 979__ 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_ 980_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ truncate - _verus_
external_ ⚠fn_ specification_ 981_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ resize - _verus_
external_ ⚠fn_ specification_ 982__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A1_ 32__ 62__ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ Vec_ 32__ 60__ 32_ U_ 44__ 32_ A2_ 32__ 62__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 983_ alloc_ 32__ 58__ 58__ 32_ vec_ 32__ 58__ 58__ 32_ from__ elem - _verus_
external_ ⚠fn_ specification_ 984_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - _verus_
external_ ⚠fn_ specification_ 985__ 60__ 32__ 38__ 32__ 39_ a_ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ iter_ 32__ 58__ 58__ 32_ Into Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - axiom_
spec_ into_ iter - axiom_
spec_ into_ iter_ borrowed - axiom_
spec_ len - axiom_
vec_ decreases_ to_ view - axiom_
vec_ has_ resolved - axiom_
vec_ index_ decreases - group_
vec_ axioms - into_
iter_ elts - lemma_
vec_ obeys_ deep_ eq - lemma_
vec_ obeys_ eq_ spec - lemma_
vec_ obeys_ view_ eq - spec_
into_ iter - spec_
into_ iter_ borrowed - spec_
vec_ len - vec_
clone_ deep_ view_ proof - vec_
clone_ trigger - vec_
index