Function extern_spec_Idx_RangeInclusive_Idx_is_empty 

pub fn extern_spec_Idx_RangeInclusive_Idx_is_empty<Idx: PartialOrd<Idx> + DeepModel>(
    self_: &RangeInclusive<Idx>,
) -> bool
where
    Idx::DeepModelTy: OrdLogic,

extern spec for RangeInclusive<Idx>::is_empty

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

ensures

result == self.is_empty_log()