| 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)
- succ# :: Nat# a -> Nat# (a + 1)
- testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
- testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b)
- testLessThan :: Nat a -> Nat b -> Maybe (a < b)
- testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)
- testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
- testZero :: Nat a -> Either (0 :=: a) (0 < a)
- testZero# :: Nat# a -> EitherVoid# (0 :=:# a) (0 <# a)
- (=?) :: Nat a -> Nat b -> Maybe (a :=: b)
- (<?) :: Nat a -> Nat b -> Maybe (a < b)
- (<?#) :: Nat# a -> Nat# b -> MaybeVoid# (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
- constant# :: forall n. KnownNat n => (# #) -> Nat# n
- zero# :: (# #) -> Nat# 0
- one# :: (# #) -> Nat# 1
- pattern N0# :: Nat# 0
- pattern N1# :: Nat# 1
- pattern N2# :: Nat# 2
- pattern N3# :: Nat# 3
- pattern N4# :: Nat# 4
- pattern N5# :: Nat# 5
- pattern N6# :: Nat# 6
- pattern N7# :: Nat# 7
- pattern N8# :: Nat# 8
- pattern N16# :: Nat# 16
- pattern N32# :: Nat# 32
- pattern N64# :: Nat# 64
- pattern N128# :: Nat# 128
- pattern N256# :: Nat# 256
- pattern N512# :: Nat# 512
- pattern N1024# :: Nat# 1024
- pattern N2048# :: Nat# 2048
- pattern N4096# :: Nat# 4096
- demote :: Nat n -> Int
- demote# :: Nat# n -> Int#
- unlift :: Nat n -> Nat# n
- lift :: Nat# n -> Nat n
- with :: Int -> (forall n. Nat n -> a) -> a
- 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
testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b) Source #
testLessThan :: Nat a -> Nat b -> Maybe (a < b) Source #
Is the first argument strictly less than the second argument?
testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b) Source #
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.