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_ 1083_ Range_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1084_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1085_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1086_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1087__ 60__ 32_ Range_ 32__ 60__ 32_ A_ 32__ 62__ 32_ as_ 32_ Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 1088__ 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_ 1089__ 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_ 1090__ 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_ 1091__ 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_ 1092__ 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_ 1093__ 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_ 1094__ 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_ 1095__ 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_ 1096__ 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_ 1097__ 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_ 1098__ 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_ 1099__ 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_ 1100__ 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_ 1101__ 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