Trait RangeInclusiveExt 

pub trait RangeInclusiveExt<Idx> {
    // Required methods
    fn start_log(self) -> Idx;
    fn end_log(self) -> Idx;
    fn is_empty_log(self) -> bool
       where Idx: DeepModel,
             Idx::DeepModelTy: OrdLogic;
}

Required Methods

fn start_log(self) -> Idx

fn end_log(self) -> Idx

fn is_empty_log(self) -> bool

where Idx: DeepModel, Idx::DeepModelTy: OrdLogic,

Implementations on Foreign Types

impl<Idx> RangeInclusiveExt<Idx> for RangeInclusive<Idx>

fn start_log(self) -> Idx

(opaque)

fn end_log(self) -> Idx

(opaque)

fn is_empty_log(self) -> bool

where Idx: DeepModel, Idx::DeepModelTy: OrdLogic,

(opaque)

ensures

!result ==> self.start_log().deep_model() <= self.end_log().deep_model()

Implementors