Arithmetic.Nat

Add two numbers.

Variant of plus for unboxed nats.

Subtract the second argument from the first argument.

Divide two numbers. Rounds down (towards zero)

Divide two numbers. Rounds up (away from zero)

Multiply two numbers.

The successor of a number.

Unlifted variant of succ.

If a natural number is greater than zero, we can operate on its predecessor.

Are the two arguments equal to one another?

Is the first argument strictly less than the second argument?

Is the first argument less-than-or-equal-to the second argument?

Is zero equal to this number or less than it?

Infix synonym of testEqual.

Infix synonym of testLessThan.

Infix synonym of testLessThanEqual.

The number zero.

The number one.

The number two.

The number three.

Use GHC's built-in type-level arithmetic to create a witness of a type-level number. This only reduces if the number is a constant.

The number zero. Unboxed.

The number one. Unboxed.

Extract the Int from a Nat. This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.

Run a computation on a witness of a type-level number. The argument Int must be greater than or equal to zero. This is not checked. Failure to upload this invariant will lead to a segfault.