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_ 1149_ Range_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1150_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 1151_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 1152_ Range Inclusive_ 32__ 58__ 58__ 32__ 60__ 32_ Idx_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 1153__ 60__ 32_ Range_ 32__ 60__ 32_ A_ 32__ 62__ 32_ as_ 32_ Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 1154__ 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_ 1155__ 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_ 1156__ 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_ 1157__ 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_ 1158__ 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_ 1159__ 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_ 1160__ 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_ 1161__ 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_ 1162__ 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_ 1163__ 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_ 1164__ 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_ 1165__ 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_ 1166__ 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_ 1167__ 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