IndexSpec

vstd::std_specs::core

Trait IndexSpec 

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

Required Methods§

Source

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

Implementors§

Source§

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