Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 1094_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 1095_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1096__ 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_ 1097_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ new__ in - _verus_
external_ ⚠fn_ specification_ 1098_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 1099_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ in - _verus_
external_ ⚠fn_ specification_ 1100_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 1101_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ try__ reserve - _verus_
external_ ⚠fn_ specification_ 1102_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 1103_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 1104_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ append - _verus_
external_ ⚠fn_ specification_ 1105_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ extend__ from__ slice - _verus_
external_ ⚠fn_ specification_ 1106_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1107_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ swap__ remove - _verus_
external_ ⚠fn_ specification_ 1108_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 1109__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1110_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 1111_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 1112_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ as__ slice - _verus_
external_ ⚠fn_ specification_ 1114__ 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_ 1115__ 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_ 1116_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ split__ off - _verus_
external_ ⚠fn_ specification_ 1117__ 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_ 1118_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ truncate - _verus_
external_ ⚠fn_ specification_ 1119_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ resize - _verus_
external_ ⚠fn_ specification_ 1120__ 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_ 1121_ alloc_ 32__ 58__ 58__ 32_ vec_ 32__ 58__ 58__ 32_ from__ elem - _verus_
external_ ⚠fn_ specification_ 1122_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - _verus_
external_ ⚠fn_ specification_ 1123__ 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