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_1056_Range_32__58__58__32__60__32_Idx_32__62__32__58__58__32_contains^⚠

_verus_external_fn_specification_1057_RangeInclusive_32__58__58__32__60__32_Idx_32__62__32__58__58__32_contains^⚠

_verus_external_fn_specification_1058_RangeInclusive_32__58__58__32__60__32_Idx_32__62__32__58__58__32_new^⚠

_verus_external_fn_specification_1059__60__32_Range_32__60__32_A_32__62__32_as_32_Iterator_32__62__32__58__58__32_next^⚠

_verus_external_fn_specification_1060__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_1061__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_1062__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_1063__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_1064__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_1065__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_1066__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_1067__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_1068__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_1069__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_1070__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_1071__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_1072__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_1073__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