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.

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.

pred i is the index immediately before i, if i is non-zero

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.

To implement clever datastructures (for instance using bit-packing), it is useful to manipulate indices as integers. See IndexSet or IndexMap for usage examples. Refrain from using it if you are not sure of what you are doing since this can break some modular abstraction.