Safe Haskell	None
Language	Haskell2010

Arithmetic.Nat

Contents

Addition
Subtraction
Division
Multiplication
Successor
Compare
Constants
Unboxed Constants
Unboxed Pattern Synonyms
Convert
Substitute

Synopsis

plus :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
plus# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> Nat# (a + b)
monus :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (Difference a b)
divide :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (Div a b)
divideRoundingUp :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (Div (a - 1) b + 1)
times :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a * b)
succ :: forall (a :: Nat). Nat a -> Nat (a + 1)
succ# :: forall (a :: Nat). Nat# a -> Nat# (a + 1)
testEqual :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a :=: b)
testEqual# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a :=:# b)
testLessThan :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
testLessThan# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <# b)
testLessThanEqual :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a <= b)
testLessThanEqual# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <=# b)
testZero :: forall (a :: Nat). Nat a -> Either (0 :=: a) (0 < a)
testZero# :: forall (a :: Nat). Nat# a -> EitherVoid# (0 :=:# a) (0 <# a)
(=?) :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a :=: b)
(<?) :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
(<?#) :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <# b)
(<=?) :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a <= b)
(<=?#) :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <=# b)
zero :: Nat 0
one :: Nat 1
two :: Nat 2
three :: Nat 3
constant :: forall (n :: Nat). KnownNat n => Nat n
constant# :: forall (n :: Nat). 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
pattern N8192# :: Nat# 8192
pattern N16384# :: Nat# 16384
demote :: forall (n :: Nat). Nat n -> Int
demote# :: forall (n :: Nat). Nat# n -> Int#
unlift :: forall (n :: Nat). Nat n -> Nat# n
lift :: forall (n :: Nat). Nat# n -> Nat n
with :: Int -> (forall (n :: Nat). Nat n -> a) -> a
with# :: Int# -> (forall (n :: Nat). Nat# n -> a) -> a
substitute# :: forall (m :: Nat) (n :: Nat). (m :=:# n) -> Nat# m -> Nat# n

Addition

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

Add two numbers.

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

Variant of plus for unboxed nats.

Subtraction

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

Subtract the second argument from the first argument.

Division

divide :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (Div a b) Source #

Divide two numbers. Rounds down (towards zero)

divideRoundingUp :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (Div (a - 1) b + 1) Source #

Divide two numbers. Rounds up (away from zero)

Multiplication

times :: forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a * b) Source #

Multiply two numbers.

Successor

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

The successor of a number.

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

Unlifted variant of succ.

Compare

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

Are the two arguments equal to one another?

testEqual# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a :=:# b) Source #

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

Is the first argument strictly less than the second argument?

testLessThan# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <# b) Source #

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

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

testLessThanEqual# :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <=# b) Source #

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

Is zero equal to this number or less than it?

testZero# :: forall (a :: Nat). Nat# a -> EitherVoid# (0 :=:# a) (0 <# a) Source #

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

Infix synonym of testEqual.

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

Infix synonym of testLessThan.

(<?#) :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <# b) Source #

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

Infix synonym of testLessThanEqual.

(<=?#) :: forall (a :: Nat) (b :: Nat). Nat# a -> Nat# b -> MaybeVoid# (a <=# b) Source #

Constants

zero :: Nat 0 Source #

The number zero.

one :: Nat 1 Source #

The number one.

two :: Nat 2 Source #

The number two.

three :: Nat 3 Source #

The number three.

constant :: forall (n :: Nat). 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.

constant# :: forall (n :: Nat). KnownNat n => (# #) -> Nat# n Source #

Unboxed Constants

zero# :: (# #) -> Nat# 0 Source #

The number zero. Unboxed.

one# :: (# #) -> Nat# 1 Source #

The number one. Unboxed.

Unboxed Pattern Synonyms

pattern N0# :: Nat# 0 Source #

pattern N1# :: Nat# 1 Source #

pattern N2# :: Nat# 2 Source #

pattern N3# :: Nat# 3 Source #

pattern N4# :: Nat# 4 Source #

pattern N5# :: Nat# 5 Source #

pattern N6# :: Nat# 6 Source #

pattern N7# :: Nat# 7 Source #

pattern N8# :: Nat# 8 Source #

pattern N16# :: Nat# 16 Source #

pattern N32# :: Nat# 32 Source #

pattern N64# :: Nat# 64 Source #

pattern N128# :: Nat# 128 Source #

pattern N256# :: Nat# 256 Source #

pattern N512# :: Nat# 512 Source #

pattern N1024# :: Nat# 1024 Source #

pattern N2048# :: Nat# 2048 Source #

pattern N4096# :: Nat# 4096 Source #

pattern N8192# :: Nat# 8192 Source #

pattern N16384# :: Nat# 16384 Source #

Convert

demote :: forall (n :: Nat). 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.

demote# :: forall (n :: Nat). Nat# n -> Int# Source #

unlift :: forall (n :: Nat). Nat n -> Nat# n Source #

lift :: forall (n :: Nat). Nat# n -> Nat n Source #

with :: Int -> (forall (n :: Nat). 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.

with# :: Int# -> (forall (n :: Nat). Nat# n -> a) -> a Source #

Substitute

substitute# :: forall (m :: Nat) (n :: Nat). (m :=:# n) -> Nat# m -> Nat# n Source #