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?

(=?) :: 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.

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.

Demote

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.