flux_core/ops/
index.rs

1use flux_attrs::*;
2
3#[extern_spec(core::ops)]
4trait Index<Idx> {
5    #![reft(fn in_bounds(v: Self, idx: Idx) -> bool { true })]
6
7    #[sig(fn(self: &Self[@v], index: Idx { <Self as Index<Idx>>::in_bounds(v, index) }) -> &Self::Output)]
8    fn index(&self, index: Idx) -> &Self::Output;
9}