Indexing
x[i1, i2, ...] applies one index per leading axis of x; axes without an index are kept. More indices than axes is E0403.
| Index | Example | Effect on the axis |
|---|---|---|
integer number or [] integer tensor | x[0] | Removed |
| integer tensor with axes | emb[ids] with ids: [b t] | Replaced by the index’s axes. If the index is Index[V], V must be this axis’s size (E0507) |
Mask tensor of rank r | x[keep] | The next r axes, which must have the mask’s sizes (E0401), are replaced by one axis of unknown size ?k |
slice lo:hi:step | x[:, 0:n-1] | See below |
Anything else as an index is E0406.
Slices. Each part is optional and must be an integer (E0406). When the bounds and the step are sizes (numbers, dims, axis names, and sums and products of them), the slice has an exact size if the checker can prove that it fits in the axis, assuming that axes aren’t empty (generic sizes at least 1, unknown sizes at least 0). A bound that is surely negative counts from the end, as in Python. So on an axis n, 0:n-1, 1: and :-1 all have size n-1, and 0:2*h:2 on (2 h) has size h. When every size is known, bounds past the ends are clamped as in Python: x[0:1000] on a [100 D] is [100 D]. Otherwise, as for 0:3 on an axis n that may be shorter than 3, or for bounds that are run-time values, the slice has a new unknown size, and no run-time check is added.
causal[n m] is a [n m] Mask that is true where the m index is at most the n index. Its two entries must be axis names in scope (E0301); anything else is E0406. Only causal takes axis names separated by spaces.