Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 567_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 568_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 569_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ new__ in - _verus_
external_ ⚠fn_ specification_ 570_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 571_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ in - _verus_
external_ ⚠fn_ specification_ 572_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 573_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 574_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 575_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ append - _verus_
external_ ⚠fn_ specification_ 576_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ extend__ from__ slice - _verus_
external_ ⚠fn_ specification_ 577_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ swap__ remove - _verus_
external_ ⚠fn_ specification_ 578_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 579__ 60__ 32_ Vec_ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 580_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 581_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 582_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ as__ slice - _verus_
external_ ⚠fn_ specification_ 583__ 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_ 584_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ split__ off - _verus_
external_ ⚠fn_ specification_ 585__ 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_ 586_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ truncate - _verus_
external_ ⚠fn_ specification_ 587_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ resize - _verus_
external_ ⚠fn_ specification_ 588__ 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_ 589_ Into Iter_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 590_ alloc_ 32__ 58__ 58__ 32_ vec_ 32__ 58__ 58__ 32_ from__ elem - _verus_
external_ ⚠fn_ specification_ 591_ Vec_ 32__ 58__ 58__ 32__ 60__ 32_ T_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - axiom_
spec_ into_ iter - axiom_
spec_ len - axiom_
vec_ index_ decreases - group_
vec_ axioms - lemma_
vec_ obeys_ deep_ eq - lemma_
vec_ obeys_ eq_ spec - lemma_
vec_ obeys_ view_ eq - spec_
into_ iter - spec_
vec_ len - vec_
clone_ deep_ view_ proof - vec_
clone_ trigger - vec_
index