Function extern_spec_std_ops_RangeBounds_T_is_empty 

pub fn extern_spec_std_ops_RangeBounds_T_is_empty<Self_, T>(
    self_: &Self_,
) -> bool
where
    T: PartialOrd + ?Sized + DeepModel,
    Self_: RangeBounds<T> + ?Sized,
    T::DeepModelTy: OrdLogic,

extern spec for ::std::ops::RangeBounds::is_empty

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

ensures

!exists<item: T::DeepModelTy> between(self.start_bound_logic().deep_model(), item, self.end_bound_logic().deep_model())