vstd
In vstd::
std_
specs::
range
Structs
ExRange
RangeGhostIterator
Traits
StepSpec
Functions
_verus_external_fn_specification_223_Range_32__58__58__32__60__32_A_32__62__32__58__58__32_next
axiom_spec_range_next_i128
axiom_spec_range_next_i16
axiom_spec_range_next_i32
axiom_spec_range_next_i64
axiom_spec_range_next_i8
axiom_spec_range_next_isize
axiom_spec_range_next_u128
axiom_spec_range_next_u16
axiom_spec_range_next_u32
axiom_spec_range_next_u64
axiom_spec_range_next_u8
axiom_spec_range_next_usize
group_range_axioms
spec_range_next
?
Settings
Function
vstd
::
std_specs
::
range
::
spec_range_next
Copy item path
source
·
[
−
]
pub
uninterp
fn spec_range_next<A>(a:
Range
<A>) -> (
Range
<A>,
Option
<A>)
Expand description