Structs§
Traits§
- Contains
Spec - ExRange
Bounds - Specification for
core::ops::RangeBounds, exposing spec-mode modelsspec_start_boundandspec_end_boundof the trait’sstart_bound/end_boundmethods. This mirrors std’s normalization of an arbitrary range into a pair of bounds and is the model used by<[T]>::copy_within(seevstd::std_specs::slice). Implementations must return these spec bounds fromstart_bound/end_bound, since std’scopy_withincalls those methods. - Range
Bounds Spec - Range
Bounds Spec Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 1164_ Range_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1165_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1166_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1167_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1168__ 60__ 32_ Range_ 32__ 60__ 32_ A_ 32__ 62__ 32_ as_ 32_ Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 1169__ 60__ 32_ Range_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1170__ 60__ 32_ Range_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1171__ 60__ 32_ Range Full_ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1172__ 60__ 32_ Range Full_ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1173__ 60__ 32_ Range From_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1174__ 60__ 32_ Range From_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1175__ 60__ 32_ Range To_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1176__ 60__ 32_ Range To_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1177__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1178__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1179__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1180__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ T_ 32__ 62__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - _verus_
external_ ⚠fn_ specification_ 1181__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ T_ 32__ 62__ 41__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ start__ bound - _verus_
external_ ⚠fn_ specification_ 1182__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ T_ 32__ 62__ 41__ 32_ as_ 32_ Range Bounds_ 32__ 60__ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ end__ bound - axiom_
i8_ obeys_ range_ step_ spec - axiom_
i16_ obeys_ range_ step_ spec - axiom_
i32_ obeys_ range_ step_ spec - axiom_
i64_ obeys_ range_ step_ spec - axiom_
i128_ obeys_ range_ step_ spec - axiom_
isize_ obeys_ range_ step_ spec - axiom_
range_ inclusive_ empty_ contains - axiom_
range_ inclusive_ out_ of_ order - axiom_
spec_ range_ next_ i8 - axiom_
spec_ range_ next_ i16 - axiom_
spec_ range_ next_ i32 - axiom_
spec_ range_ next_ i64 - axiom_
spec_ range_ next_ i128 - axiom_
spec_ range_ next_ isize - axiom_
spec_ range_ next_ u8 - axiom_
spec_ range_ next_ u16 - axiom_
spec_ range_ next_ u32 - axiom_
spec_ range_ next_ u64 - axiom_
spec_ range_ next_ u128 - axiom_
spec_ range_ next_ usize - axiom_
u8_ obeys_ range_ step_ spec - axiom_
u16_ obeys_ range_ step_ spec - axiom_
u32_ obeys_ range_ step_ spec - axiom_
u64_ obeys_ range_ step_ spec - axiom_
u128_ obeys_ range_ step_ spec - axiom_
usize_ obeys_ range_ step_ spec - bound_
as_ ref - group_
range_ axioms - obeys_
range_ step_ spec - slice_
range_ end - slice_
range_ start - slice_
range_ valid - spec_
range_ inclusive_ end_ bound - spec_
range_ inclusive_ is_ empty - spec_
range_ inclusive_ len - spec_
range_ inclusive_ out_ of_ order - spec_
range_ inclusive_ start_ bound - spec_
range_ inclusive_ unspecified_ bounds - spec_
range_ inclusive_ unspecified_ contains - spec_
range_ inclusive_ unspecified_ ref_ bounds - spec_
range_ next