Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 806_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 807_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 808__ 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_ 809_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ new__ in - _verus_
external_ ⚠fn_ specification_ 810_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 811_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ in - _verus_
external_ ⚠fn_ specification_ 812_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 813_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ try__ reserve - _verus_
external_ ⚠fn_ specification_ 814_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 815_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 816_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ append - _verus_
external_ ⚠fn_ specification_ 817_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ extend__ from__ slice - _verus_
external_ ⚠fn_ specification_ 818_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 819_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ swap__ remove - _verus_
external_ ⚠fn_ specification_ 820_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 821__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 822_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 823_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 824_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ as__ slice - _verus_
external_ ⚠fn_ specification_ 826__ 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_ 827__ 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_ 828_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ split__ off - _verus_
external_ ⚠fn_ specification_ 829__ 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_ 830_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ truncate - _verus_
external_ ⚠fn_ specification_ 831_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ resize - _verus_
external_ ⚠fn_ specification_ 832__ 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_ 833_ alloc_ 32__ 58__ 58__ 32_ vec_ 32__ 58__ 58__ 32_ from__ elem - _verus_
external_ ⚠fn_ specification_ 834_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - _verus_
external_ ⚠fn_ specification_ 835__ 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