Arithmetic.Types

A value-level representation of a natural number n.

Unboxed variant of Nat.

Proof that the first argument can be expressed as the sum of the second argument and some other natural number.

A finite set of n elements. 'Fin n = { 0 .. n - 1 }'

Finite numbers without the overhead of carrying around a proof.

Variant of Fin# that only allows 32-bit integers.

Either a Fin# or Nothing. Internally, this uses negative one to mean Nothing.

Either a Fin# bounded by the left natural or one bounded by the right natural.

Proof that the first argument is strictly less than the second argument.

Proof that the first argument is less than or equal to the second argument.

Proof that the first argument is equal to the second argument.