Module Indexing.IndexSource

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.

• raises Invalid_argument

  if the index i is out of bounds.

to_int casts an index i back to an ordinary integer value.

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.