Trait RangeInclusiveExt 

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

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", so this trait is not object safe.

Implementations on Foreign Types

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

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

logic(opaque)

ensures

start == result.start_log() && end == result.end_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