| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Arithmetic.Nat
Synopsis
- plus :: Nat a -> Nat b -> Nat (a + b)
- plus# :: Nat# a -> Nat# b -> Nat# (a + b)
- monus :: Nat a -> Nat b -> Maybe (Difference a b)
- divide :: Nat a -> Nat b -> Nat (Div a b)
- divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1)
- times :: Nat a -> Nat b -> Nat (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
- zero# :: (# #) -> Nat# 0
- demote :: Nat n -> Int
- unlift :: Nat n -> Nat# n
- lift :: Nat# n -> Nat n
- 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.
Division
divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1) Source #
Divide two numbers. Rounds up (away from zero)
Multiplication
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.