Trait RangeInclusiveExt 

pub trait RangeInclusiveExt<Idx> {
    // Required methods
    fn new_log(start: Idx, end: Idx) -> Self
       where Idx: DeepModel,
             Idx::DeepModelTy: OrdLogic;
    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 new_log(start: Idx, end: Idx) -> Self

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

logic

fn start_log(self) -> Idx

logic

fn end_log(self) -> Idx

logic

fn is_empty_log(self) -> bool

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

logic

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

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

fn new_log(start: Idx, end: Idx) -> Self

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

logic(opaque)

ensures

start == result.start_log()

ensures

end == result.end_log()

ensures

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

fn start_log(self) -> Idx

logic(opaque)

fn end_log(self) -> Idx

logic(opaque)

fn is_empty_log(self) -> bool

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

logic(opaque)

ensures

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

Implementors