Structs§
Functions§
- _verus_
external_ ⚠fn_ specification_ 1178__ 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_ 1179__ 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_ 1180__ 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_ 1181__ 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_ 1182__ 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_ 1183__ 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_ 1184__ 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_ 1185__ 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_ 1186__ 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_ 1187__ 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_ 1188__ 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_ 1189__ 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_ 1190__ 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_ 1191__ 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_ 1192__ 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_ 1193__ 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_ 1194__ 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_ 1195__ 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_ 1196__ 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_ 1197__ 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_ 1198__ 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_ 1199__ 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_ 1200__ 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_ 1201__ 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_ 1202__ 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_ 1203__ 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_ 1204__ 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_ 1205__ 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_ 1206__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ starts__ with - _verus_
external_ ⚠fn_ specification_ 1207__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ ends__ with - _verus_
external_ ⚠fn_ specification_ 1208__ 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_ 1209__ 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_ 1210__ 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_ 1211__ 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_ 1212__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 1213__ 60__ 32__ 91_ T_ 59__ 32_ N_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 1214_ core_ 32__ 58__ 58__ 32_ hint_ 32__ 58__ 58__ 32_ unreachable__ unchecked - _verus_
external_ ⚠fn_ specification_ 1215__ 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_ 1216__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1217__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ reverse - _verus_
external_ ⚠fn_ specification_ 1218__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 1219__ 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_ 1220__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ iter__ mut - _verus_
external_ ⚠fn_ specification_ 1221__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ first - _verus_
external_ ⚠fn_ specification_ 1222__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ last - _verus_
external_ ⚠fn_ specification_ 1225__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at - _verus_
external_ ⚠fn_ specification_ 1227__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ at__ checked - _verus_
external_ ⚠fn_ specification_ 1228__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ first - _verus_
external_ ⚠fn_ specification_ 1229__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ split__ first__ mut - _verus_
external_ ⚠fn_ specification_ 1230__ 60__ 32__ 91_ T_ 93__ 32__ 62__ 32__ 58__ 58__ 32_ copy__ from__ slice - _verus_
external_ ⚠fn_ specification_ 1231__ 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_ 1232__ 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_
slice_ contains - spec_
slice_ ends_ with - spec_
slice_ starts_ with