Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- plus :: Nat a -> Nat b -> Nat (a + b)
- monus :: Nat a -> Nat b -> Maybe (Difference a b)
- succ :: Nat a -> Nat (a + 1)
- testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
- testLessThan :: Nat a -> Nat b -> Maybe (a < b)
- testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
- testZero :: Nat a -> Either (0 :=: a) (0 < a)
- (=?) :: Nat a -> Nat b -> Maybe (a :=: b)
- (<?) :: Nat a -> Nat b -> Maybe (a < b)
- (<=?) :: Nat a -> Nat b -> Maybe (a <= b)
- zero :: Nat 0
- one :: Nat 1
- two :: Nat 2
- three :: Nat 3
- constant :: forall n. KnownNat n => Nat n
- demote :: Nat n -> Int
- with :: Int -> (forall n. Nat n -> a) -> a

# Addition

# Subtraction

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

Subtract the second argument from the first argument.

# Successor

# Compare

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?

# Constants

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.