Function extern_spec_std_ops_Idx_RangeInclusive_Idx_new 

pub fn extern_spec_std_ops_Idx_RangeInclusive_Idx_new<Idx>(
    start: Idx,
    end: Idx,
) -> RangeInclusive<Idx>
where
    Idx: DeepModel,
    Idx::DeepModelTy: OrdLogic,

extern spec for ::std::ops::RangeInclusive<Idx>::new

This is not a real function: its only use is for documentation.

ensures

result.start_log() == start

ensures

result.end_log() == end

ensures

start.deep_model() <= end.deep_model() ==> !result.is_empty_log()