flux_core/ops/
index.rs

1use flux_attrs::*;
2
3/// See the note at [`IndexMut`] about also implementing the [`index_mut`] method for any type that implements [`Index`].
4#[extern_spec(core::ops)]
5trait Index<Idx> {
6    #![assoc(fn in_bounds(v: Self, idx: Idx) -> bool { true })]
7    #![assoc(fn output_pred(v: Self, idx: Idx, out: Self::Output) -> bool { true })]
8
9    #[sig(fn(self: &Self[@v], index: Idx { <Self as Index<Idx>>::in_bounds(v, index) }) -> &Self::Output{out: <Self as Index<Idx>>::output_pred(v, index, out)})]
10    fn index(&self, index: Idx) -> &Self::Output;
11}
12
13/// [NOTE:The [`IndexMut`] trait is a subtrait of [`Index`],
14/// hence any (refined) impl of `Index` should now *also*
15/// have a matching (refined) impl for `IndexMut` as otherwise
16/// the latter will either
17/// - fail the impl-subtyping, (e.g. in the case of regular specs), or worse
18/// - be silently inconsistent (e.g. in the case of extern-specs).
19#[extern_spec(core::ops)]
20trait IndexMut<Idx>: Index<Idx> {
21    #[sig(fn(self: &mut Self[@v], index: Idx { <Self as Index<Idx>>::in_bounds(v, index) }) -> &mut Self::Output{out: <Self as Index<Idx>>::output_pred(v, index, out)})]
22    fn index_mut(&mut self, index: Idx) -> &mut Self::Output;
23}
flux_core/ops/index.rs

flux_core/ops/
index.rs
