Arithmetic.Nat

Addition

plus :: Nat a -> Nat b -> Nat (a + b)

Add two numbers.

Subtraction

monus :: Nat a -> Nat b -> Maybe (Difference a b)

Subtract the second argument from the first argument.

Successor

succ :: Nat a -> Nat (a + 1)

The successor of a number.

Compare

testEqual :: Nat a -> Nat b -> Maybe (a :=: b)

Are the two arguments equal to one another?

testLessThan :: Nat a -> Nat b -> Maybe (a < b)

Is the first argument strictly less than the second argument?

testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)

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

testZero :: Nat a -> Either (0 :=: a) (0 < a)

Is zero equal to this number or less than it?

(=?) :: Nat a -> Nat b -> Maybe (a :=: b)

Infix synonym of testEqual.

(<?) :: Nat a -> Nat b -> Maybe (a < b)

Infix synonym of testLessThan.

(<=?) :: Nat a -> Nat b -> Maybe (a <= b)

Infix synonym of testLessThanEqual.

Constants

zero :: Nat 0

The number zero.

one :: Nat 1

The number one.

two :: Nat 2

The number two.

three :: Nat 3

The number three.

constant :: forall n. KnownNat n => Nat n

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.

Convert

demote :: Nat n -> Int

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.

with :: Int -> (forall n. Nat n -> a) -> a

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.