Structs§
Functions§
- _verus_
external_ ⚠fn_ specification_ 1112__ 60__ 32_ usize_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1113__ 60__ 32_ usize_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1114__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1115__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1116__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1117__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1118__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1119__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1120__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1121__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1122__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1123__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1124__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1125__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1126__ 60__ 32__ 91_ T_ 93__ 32_ as_ 32_ Index_ 32__ 60__ 32_ I_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1127__ 60__ 32__ 91_ T_ 93__ 32_ as_ 32_ Index Mut_ 32__ 60__ 32_ I_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1128__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1129__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1130_ core_ 32__ 58__ 58__ 32_ hint_ 32__ 58__ 58__ 32_ unreachable__ unchecked - _verus_
external_ ⚠fn_ specification_ 1131__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 1132__ 60__ 32__ 38__ 32__ 39_ a_ 32__ 91_ T_ 93__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ iter_ 32__ 58__ 58__ 32_ Into Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - _verus_
external_ ⚠fn_ specification_ 1133__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ first - _verus_
external_ ⚠fn_ specification_ 1134__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ last - _verus_
external_ ⚠fn_ specification_ 1137__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at - _verus_
external_ ⚠fn_ specification_ 1139__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at__ checked - _verus_
external_ ⚠fn_ specification_ 1140__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ copy__ from__ slice - _verus_
external_ ⚠fn_ specification_ 1141__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ copy__ within_ 32__ 58__ 58__ 32__ 60__ 32_ R_ 32__ 62_ - axiom_
slice_ get_ range - axiom_
slice_ get_ range_ from - axiom_
slice_ get_ range_ full - axiom_
slice_ get_ range_ inclusive - axiom_
slice_ get_ range_ to - axiom_
slice_ get_ range_ to_ inclusive - copy_
within_ result - group_
slice_ axioms - into_
iter_ elts