Skip to main content

spec_range_inclusive_out_of_order

vstd::std_specs::range

Function spec_range_inclusive_out_of_order 

Source 
pub uninterp spec fn spec_range_inclusive_out_of_order<Idx>(r: &RangeInclusive<Idx>) -> bool
Expand description

Uninterpreted because RangeBounds methods have no PartialOrd bound. Defined by axiom_range_inclusive_out_of_order.