Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 1233_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 1234_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1235__ 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_ 1236_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ new__ in - _verus_
external_ ⚠fn_ specification_ 1237_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 1238_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ in - _verus_
external_ ⚠fn_ specification_ 1239_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 1240_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ try__ reserve - _verus_
external_ ⚠fn_ specification_ 1241_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ try__ reserve__ exact - _verus_
external_ ⚠fn_ specification_ 1242_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 1243_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 1244_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ append - _verus_
external_ ⚠fn_ specification_ 1245_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ extend__ from__ slice - _verus_
external_ ⚠fn_ specification_ 1246_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1247_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ swap__ remove - _verus_
external_ ⚠fn_ specification_ 1248_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 1249__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1250_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 1251_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 1252_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ as__ slice - _verus_
external_ ⚠fn_ specification_ 1254__ 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_ 1255__ 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_ 1256_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ split__ off - _verus_
external_ ⚠fn_ specification_ 1257__ 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_ 1258_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ truncate - _verus_
external_ ⚠fn_ specification_ 1259_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ resize - _verus_
external_ ⚠fn_ specification_ 1260__ 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_ 1261_ alloc_ 32__ 58__ 58__ 32_ vec_ 32__ 58__ 58__ 32_ from__ elem - _verus_
external_ ⚠fn_ specification_ 1262_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - _verus_
external_ ⚠fn_ specification_ 1263__ 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_ 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_
vec_ len - tracked_
borrow_ mut_ slice - tracked_
borrow_ slice - vec_
clone_ deep_ view_ proof - vec_
clone_ trigger - vec_
index