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). - Range
Bounds Spec - Range
Bounds Spec Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 1126_ Range_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1127_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1128_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1129_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1130__ 60__ 32_ Range_ 32__ 60__ 32_ A_ 32__ 62__ 32_ as_ 32_ Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 1131__ 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_ 1132__ 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_ 1133__ 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_ 1134__ 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_ 1135__ 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_ 1136__ 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_ 1137__ 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_ 1138__ 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_ 1139__ 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_ 1140__ 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_ 1141__ 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_ 1142__ 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_ 1143__ 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_ 1144__ 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_
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 - bound_
as_ ref - group_
range_ axioms - slice_
range_ end - slice_
range_ start - slice_
range_ valid - spec_
range_ inclusive_ end_ bound - spec_
range_ inclusive_ is_ empty - spec_
range_ next