Function extern_spec_T_From_RangeInclusive_T_legacy_RangeInclusive_T_from 

pub fn extern_spec_T_From_RangeInclusive_T_legacy_RangeInclusive_T_from<T>(
    value: RangeInclusive<T>,
) -> RangeInclusive<T>
where
    T: DeepModel<DeepModelTy: OrdLogic>,

extern spec for legacy::RangeInclusive<T>::from

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

ensures

result.start_log() == value.start

ensures

result.end_log() == value.last

ensures

value.start.deep_model() <= value.last.deep_model() ==> !result.is_empty_log()