-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Type-level integers, using TypeNats, Data
--   Kinds, and Closed Type Families.
--   
--   This package provides type level representations of the (positive and
--   negative) integers and basic operations (addition, subtraction,
--   multiplication, division, exponentiation) on these. The numtype-dk
--   package differs from the numtype package in that the NumTypes are
--   implemented using Data Kinds, TypeNats, and Closed Type Families
--   rather than Functional Dependencies. Requires GHC 7.8 or later.
@package numtype-dk
@version 0.5.0.3

-- | 
Summary
--   
--   Type-level integers for GHC 7.8+.
--   
--   We provide type level arithmetic operations. We also provide
--   term-level arithmetic operations on proxys, and conversion from the
--   type level to the term level.
--   
--   
Planned Obsolesence
--   
--   We commit this package to hackage in sure and certain hope of the
--   coming of glorious GHC integer type literals, when the sea shall give
--   up her dead, and this package shall be rendered unto obsolescence.
module Numeric.NumType.DK.Integers
data TypeInt
Neg10Minus :: Nat -> TypeInt
Neg9 :: TypeInt
Neg8 :: TypeInt
Neg7 :: TypeInt
Neg6 :: TypeInt
Neg5 :: TypeInt
Neg4 :: TypeInt
Neg3 :: TypeInt
Neg2 :: TypeInt
Neg1 :: TypeInt
Zero :: TypeInt
Pos1 :: TypeInt
Pos2 :: TypeInt
Pos3 :: TypeInt
Pos4 :: TypeInt
Pos5 :: TypeInt
Pos6 :: TypeInt
Pos7 :: TypeInt
Pos8 :: TypeInt
Pos9 :: TypeInt
Pos10Plus :: Nat -> TypeInt
type family Pred (i :: TypeInt) :: TypeInt
type family Succ (i :: TypeInt) :: TypeInt

-- | TypeInt negation.
type family Negate (i :: TypeInt) :: TypeInt

-- | Absolute value.
type family Abs (i :: TypeInt) :: TypeInt

-- | Signum.
type family Signum (i :: TypeInt) :: TypeInt

-- | TypeInt addition.
type family (i :: TypeInt) + (i' :: TypeInt) :: TypeInt
infixl 6 +

-- | TypeInt subtraction.
type family (i :: TypeInt) - (i' :: TypeInt) :: TypeInt
infixl 6 -

-- | TypeInt multiplication.
type family (i :: TypeInt) * (i' :: TypeInt) :: TypeInt
infixl 7 *

-- | TypeInt division.
type family (i :: TypeInt) / (i' :: TypeInt) :: TypeInt
infixl 7 /

-- | TypeInt exponentiation.
type family (i :: TypeInt) ^ (i' :: TypeInt) :: TypeInt
infixr 8 ^
pred :: forall (i :: TypeInt). Proxy i -> Proxy (Pred i)
succ :: forall (i :: TypeInt). Proxy i -> Proxy (Succ i)
negate :: forall (i :: TypeInt). Proxy i -> Proxy (Negate i)
abs :: forall (i :: TypeInt). Proxy i -> Proxy (Abs i)
signum :: forall (i :: TypeInt). Proxy i -> Proxy (Signum i)
(+) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i + i')
infixl 6 +
(-) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i - i')
infixl 6 -
(*) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i * i')
infixl 7 *
(/) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i / i')
infixl 7 /
(^) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i ^ i')
infixr 8 ^
zero :: Proxy 'Zero
pos1 :: Proxy 'Pos1
pos2 :: Proxy 'Pos2
pos3 :: Proxy 'Pos3
pos4 :: Proxy 'Pos4
pos5 :: Proxy 'Pos5
pos6 :: Proxy 'Pos6
pos7 :: Proxy 'Pos7
pos8 :: Proxy 'Pos8
pos9 :: Proxy 'Pos9
neg1 :: Proxy 'Neg1
neg2 :: Proxy 'Neg2
neg3 :: Proxy 'Neg3
neg4 :: Proxy 'Neg4
neg5 :: Proxy 'Neg5
neg6 :: Proxy 'Neg6
neg7 :: Proxy 'Neg7
neg8 :: Proxy 'Neg8
neg9 :: Proxy 'Neg9

-- | Conversion to a Num.
class KnownTypeInt (i :: TypeInt)
toNum :: (KnownTypeInt i, Num a) => Proxy i -> a
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg1
instance Numeric.NumType.DK.Integers.KnownTypeInt (Numeric.NumType.DK.Integers.Succ ('Numeric.NumType.DK.Integers.Neg10Minus n)) => Numeric.NumType.DK.Integers.KnownTypeInt ('Numeric.NumType.DK.Integers.Neg10Minus n)
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg2
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg3
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg4
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg5
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg6
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg7
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg8
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Neg9
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos1
instance Numeric.NumType.DK.Integers.KnownTypeInt (Numeric.NumType.DK.Integers.Pred ('Numeric.NumType.DK.Integers.Pos10Plus n)) => Numeric.NumType.DK.Integers.KnownTypeInt ('Numeric.NumType.DK.Integers.Pos10Plus n)
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos2
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos3
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos4
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos5
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos6
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos7
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos8
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Pos9
instance Numeric.NumType.DK.Integers.KnownTypeInt 'Numeric.NumType.DK.Integers.Zero
