Trait IndexSpec 

pub trait IndexSpec<Idx>: Index<Idx>
where
    Idx: ?Sized,
{
    // Required method
    spec fn index_req(&self, index: &Idx) -> bool;
}

Required Methods

spec fn index_req(&self, index: &Idx) -> bool

Dyn Compatibility

This trait is dyn compatible.

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

Implementors

impl<Idx, VERUS_SPEC__A: Index<Idx> + ?Sized> IndexSpec<Idx> for VERUS_SPEC__A

where Idx: ?Sized,