natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Arithmetic.Nat

Synopsis

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

Subtraction

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

Subtract the second argument from the first argument.

Successor

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

The successor of a number.

Compare

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

Are the two arguments equal to one another?

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

Is the first argument strictly less than the second argument?

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

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

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

Is zero equal to this number or less than it?

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

Infix synonym of testEqual.

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

Infix synonym of testLessThan.

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

Infix synonym of testLessThanEqual.

Constants

The number zero.

The number one.

The number two.

The number three.

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

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 Source #

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 Source #

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.