Module range 

Structs

ExBound

ExRange

ExRangeFrom

ExRangeFull

ExRangeInclusive

ExRangeTo

ExRangeToInclusive

RangeInclusiveView

Enums

SpecBound

Spec model of core::ops::Bound, used by RangeBoundsSpec to describe the start and end bounds of a range. See spec_bound for the connection to Bound values.

Traits

ContainsSpec

ExRangeBounds

Specification for core::ops::RangeBounds, exposing spec-mode models spec_start_bound and spec_end_bound of the trait’s start_bound/end_bound methods. This mirrors std’s normalization of an arbitrary range into a pair of bounds and is the model used by <[T]>::copy_within (see vstd::std_specs::slice).

RangeBoundsSpec

RangeBoundsSpecImpl

Functions

_verus_external_fn_specification_928_Range_32__58__58__32__60__32_Idx_32__62__32__58__58__32_contains^⚠

_verus_external_fn_specification_929_RangeInclusive_32__58__58__32__60__32_Idx_32__62__32__58__58__32_contains^⚠

_verus_external_fn_specification_930_RangeInclusive_32__58__58__32__60__32_Idx_32__62__32__58__58__32_new^⚠

_verus_external_fn_specification_931__60__32_Range_32__60__32_A_32__62__32_as_32_Iterator_32__62__32__58__58__32_next^⚠

_verus_external_fn_specification_932__60__32_Range_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_933__60__32_Range_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_934__60__32_RangeFull_32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_935__60__32_RangeFull_32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_936__60__32_RangeFrom_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_937__60__32_RangeFrom_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_938__60__32_RangeTo_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_939__60__32_RangeTo_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_940__60__32_RangeInclusive_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_941__60__32_RangeInclusive_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_942__60__32_RangeToInclusive_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_943__60__32_RangeToInclusive_32__60__32_T_32__62__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

_verus_external_fn_specification_944__60__32__40_Bound_32__60__32_T_32__62__32__44__32_Bound_32__60__32_T_32__62__41__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_start__bound^⚠

_verus_external_fn_specification_945__60__32__40_Bound_32__60__32_T_32__62__32__44__32_Bound_32__60__32_T_32__62__41__32_as_32_RangeBounds_32__60__32_T_32__62__32__62__32__58__58__32_end__bound^⚠

axiom_spec_range_inclusive_new

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

group_range_axioms

slice_range_end

slice_range_start

slice_range_valid

spec_bound

spec_bound_ref

spec_range_inclusive_new

spec_range_next