Structs§
Functions§
- _verus_
external_ ⚠fn_ specification_ 1211__ 60__ 32_ usize_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 1212__ 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_ 1213__ 60__ 32_ usize_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1214__ 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_ 1215__ 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_ get - _verus_
external_ ⚠fn_ specification_ 1216__ 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_ 1217__ 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_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1218__ 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_ 1219__ 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_ get - _verus_
external_ ⚠fn_ specification_ 1220__ 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_ 1221__ 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_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1222__ 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_ 1223__ 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_ get - _verus_
external_ ⚠fn_ specification_ 1224__ 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_ 1225__ 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_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1226__ 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_ 1227__ 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_ get - _verus_
external_ ⚠fn_ specification_ 1228__ 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_ 1229__ 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_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1230__ 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_ 1231__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 1232__ 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_ 1233__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1234__ 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_ 1235__ 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_ get - _verus_
external_ ⚠fn_ specification_ 1236__ 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_ 1237__ 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_ get__ mut - _verus_
external_ ⚠fn_ specification_ 1238__ 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_ 1239__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ starts__ with - _verus_
external_ ⚠fn_ specification_ 1240__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ ends__ with - _verus_
external_ ⚠fn_ specification_ 1241__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ I_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1242__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ I_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1243__ 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_ 1244__ 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_ 1245__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ get__ unchecked_ 32__ 58__ 58__ 32__ 60__ 32_ I_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1246__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ get__ unchecked__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ I_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1247__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1248__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1249_ core_ 32__ 58__ 58__ 32_ hint_ 32__ 58__ 58__ 32_ unreachable__ unchecked - _verus_
external_ ⚠fn_ specification_ 1250__ 60__ 32__ 91_ T_ 93__ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32__ 91_ U_ 93__ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 1251__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1252__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ reverse - _verus_
external_ ⚠fn_ specification_ 1253__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ swap - _verus_
external_ ⚠fn_ specification_ 1254__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 1255__ 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_ 1256__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ iter__ mut - _verus_
external_ ⚠fn_ specification_ 1257__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ first - _verus_
external_ ⚠fn_ specification_ 1258__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ last - _verus_
external_ ⚠fn_ specification_ 1261__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at - _verus_
external_ ⚠fn_ specification_ 1263__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at__ checked - _verus_
external_ ⚠fn_ specification_ 1264__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at__ unchecked - _verus_
external_ ⚠fn_ specification_ 1266__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ first - _verus_
external_ ⚠fn_ specification_ 1267__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ first__ mut - _verus_
external_ ⚠fn_ specification_ 1268__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ copy__ from__ slice - _verus_
external_ ⚠fn_ specification_ 1269__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ copy__ within_ 32__ 58__ 58__ 32__ 60__ 32_ R_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1270__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ chunks - after_
chunks_ elts - copy_
within_ result - generic_
slice_ in_ bounds - generic_
slice_ index_ mut_ postcondition - generic_
slice_ index_ postcondition - into_
iter_ elts - spec_
range_ inclusive_ unspecified_ slice_ in_ bounds - spec_
slice_ contains - spec_
slice_ ends_ with - spec_
slice_ starts_ with