Module Indexing.Index

The submodule Index allows safely manipulating indices into a finite set.

type 'n t = 'n index
val of_int : 'n cardinal -> int -> '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.

val to_int : 'n index -> int

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

val iter : 'n cardinal -> ('n index -> unit) -> unit

iter n yield calls yield i successively for every index in the range [0, n), in increasing order.

exception End_of_set

This exception is raised by an iterator (created by enumerate) that is queried after it has been exhausted.

val enumerate : 'n cardinal -> unit -> 'n index

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.