flux_core/ops/
index.rs

1
2
3
4
5
6
7
8
9
use flux_attrs::*;

#[extern_spec(core::ops)]
trait Index<Idx> {
    #![reft(fn in_bounds(v: Self, idx: Idx) -> bool { true })]

    #[sig(fn(self: &Self[@v], index: Idx { <Self as Index<Idx>>::in_bounds(v, index) }) -> &Self::Output)]
    fn index(&self, index: Idx) -> &Self::Output;
}