The type n finite encodes all finite sets of cardinal n. It is used by the module Linear to represent accesses to vectors and matrices coefficients, statically ensuring that no out of bounds access can be performed.

The first element of any finite subset. The type encodes that for a finite subset to have an element, its cardinal must be at least one.

last n returns a value encoding the last element of any finite subset of cardinal n.

The call next f returns a value encoding the element right after f in a finite subset. The type encodes the relations between the cardinal of the finite subset containing f and the cardinal of the one containing its successor.

The call prev f returns a value encoding the element right before f in a finite subset. The type encodes the relations between the cardinal of the finite subset containing f and the cardinal of the one containing its predecessor.

If f is an element of any finite subset of cardinal n, it is also an element of any finite subset of cardinal n + 1. The call weaken f allows to prove that fact to the type system.

If f is an element of any finite subset of cardinal n + 1, it may also be an element of any finite subset of cardinal n. The call strengten n f allows to prove that fact to the type system. None is returned if and only if f is the last element of its subset.

The call of_int limit n returns a finite value representing the n-nd element of a finite set of cardinal limit. If n is not in the bounds, None is returned. This function complexity is O(1).

The call to_int n returns an integer equal to n. This function complexity is O(1).

The call for_each f limit acc folds over each finite elements of a set of cardinal limit, computing f at each step. The function complexity is O(n).