`Indexing.Index`

The submodule `Index`

allows safely manipulating indices into a finite set.

`type 'n t = 'n index`

If `n`

is the cardinal of the type-level set `n`

, then `of_int n`

casts an integer `i`

of type `int`

into an index: that is, `of_int n i`

returns `i`

at type `n index`

. The integer `i`

must lie in the semi-open interval `[0, n)`

. This is enforced by a runtime check. Calling `of_int n i`

fixes the cardinal `n`

.

`iter n yield`

calls `yield i`

successively for every index in the range `[0, n)`

, in increasing order.

`rev_iter n yield`

calls `yield i`

successively for every index in the range `[0, n)`

, in decreasing order.

This exception is raised by an iterator (created by `enumerate`

) that is queried after it has been exhausted.

`enumerate n`

returns an imperative iterator, which produces all indices in the range `[0, n)`

in increasing order. Querying the iterator after all elements have been produced causes the exception `End_of_set`

to be raised.