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


-- | Type-level programming library
--   
--   This library permits performing computations on the type-level.
--   Type-level functions are implemented using functional dependencies of
--   multi parameter type classes. To date, Booleans and Numerals (Naturals
--   and Positives) are supported. With regard to Numerals, there is
--   support for common arithmetic operations (addition, substraction,
--   multiplication, division, exponientation, logarithm, maximum,
--   comparison, GCD) over natural numbers (using a decimal representation
--   to make compile-time errors friendlier). Although making use of
--   type-level computations might seem devious and obfuscated at first
--   sight, it is indeed useful in practice to implement lightweight
--   dependent types such us number-parameterized types (e.g. an array type
--   parameterized by the array's size or a modular group type Zn
--   parameterized by the modulus). Here is a tutorial on type-level
--   numerals and how to use them to implement numerically-parameterized
--   vectors:
--   <a>http://www.ict.kth.se/forsyde/files/tutorial/tutorial.html#FSVec</a>
@package type-level
@version 0.2.4


-- | Type-level numerical representations. Currently, only decimals are
--   supported.
module Data.TypeLevel.Num.Reps

-- | Decimal digit zero
data D0

-- | Decimal digit one
data D1

-- | Decimal digit two
data D2

-- | Decimal digit three
data D3

-- | Decimal digit four
data D4

-- | Decimal digit five
data D5

-- | Decimal digit six
data D6

-- | Decimal digit seven
data D7

-- | Decimal digit eight
data D8

-- | Decimal digit nine
data D9

-- | Connective to glue digits together. For example, <tt>D1 :* D0 :*
--   D0</tt> represents the decimal number 100
data (:*) a b
(:*) :: a -> b -> :* a b
instance Typeable D0
instance Typeable D1
instance Typeable D2
instance Typeable D3
instance Typeable D4
instance Typeable D5
instance Typeable D6
instance Typeable D7
instance Typeable D8
instance Typeable D9
instance Typeable2 :*
instance (Lift a, Lift b) => Lift (a :* b)
instance (Show a, Show b) => Show (a :* b)
instance Lift D9
instance Show D9
instance Lift D8
instance Show D8
instance Lift D7
instance Show D7
instance Show D6
instance Lift D6
instance Lift D5
instance Show D5
instance Lift D4
instance Show D4
instance Lift D3
instance Show D3
instance Lift D2
instance Show D2
instance Lift D1
instance Show D1
instance Lift D0
instance Show D0


-- | Type-level numerical sets. Currently there is only support for
--   Naturals and Positives.
module Data.TypeLevel.Num.Sets

-- | Positives (Naturals without zero)
class PosI n => Pos n

-- | Naturals (Positives and zero)
class NatI n => Nat n

-- | Reflecting function
toNum :: (NatI n, Num a) => n -> a

-- | Less generic reflecting function (Int)
toInt :: Nat n => n -> Int

-- | Reification function. In CPS style (best possible solution)
reifyIntegral :: Integral i => i -> (forall n. Nat n => n -> r) -> r
instance PosI x => PosI (x :* D9)
instance PosI x => PosI (x :* D8)
instance PosI x => PosI (x :* D7)
instance PosI x => PosI (x :* D6)
instance PosI x => PosI (x :* D5)
instance PosI x => PosI (x :* D4)
instance PosI x => PosI (x :* D3)
instance PosI x => PosI (x :* D2)
instance PosI x => PosI (x :* D1)
instance PosI x => PosI (x :* D0)
instance PosI D9
instance PosI D8
instance PosI D7
instance PosI D6
instance PosI D5
instance PosI D4
instance PosI D3
instance PosI D2
instance PosI D1
instance PosI x => NatI (x :* D9)
instance PosI x => NatI (x :* D8)
instance PosI x => NatI (x :* D7)
instance PosI x => NatI (x :* D6)
instance PosI x => NatI (x :* D5)
instance PosI x => NatI (x :* D4)
instance PosI x => NatI (x :* D3)
instance PosI x => NatI (x :* D2)
instance PosI x => NatI (x :* D1)
instance PosI x => NatI (x :* D0)
instance NatI D9
instance NatI D8
instance NatI D7
instance NatI D6
instance NatI D5
instance NatI D4
instance NatI D3
instance NatI D2
instance NatI D1
instance NatI D0
instance PosI n => Pos n
instance NatI n => Nat n


-- | Internal template haskell functions to generate type-level numeral
--   aliases
module Data.TypeLevel.Num.Aliases.TH
genAliases :: Int -> Int -> Int -> Int -> Q [Dec]

-- | Generate the type-level decimal representation for a value-level
--   natural number. NOTE: This function could be useful by itself avoiding
--   to generate aliases. However, type-splicing is not yet supported by
--   template haskell.
dec2TypeLevel :: Int -> Q Type


-- | Type synonym aliases of type-level numerals and their value-level
--   reflecting functions. Generated for user convenience.
--   
--   Aliases are generated using binary, octal, decimal and hexadecimal
--   bases. Available aliases cover binaries up to b10000000000, octals up
--   to o10000, decimals up to d5000 and hexadecimals up to h1000
module Data.TypeLevel.Num.Aliases


-- | Type-level Booleans.
module Data.TypeLevel.Bool

-- | Type-level Booleans
class BoolI b => Bool b
toBool :: BoolI b => b -> Bool

-- | False type-level value
data False

-- | False value-level reflecting function
false :: False

-- | True type-level value
data True

-- | True value-level reflecting function
true :: True

-- | Reification function. In CPS style (best possible solution)
reifyBool :: Bool -> (forall b. Bool b => b -> r) -> r

-- | Boolean negation type-level relation. <tt>Not b1 b2</tt> establishes
--   that <tt>not b1 = b2</tt>
class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1

-- | value-level reflection function for the <a>Not</a> type-level relation
not :: Not b1 b2 => b1 -> b2

-- | <a>And</a> type-level relation. <tt>And b1 b2 b3</tt> establishes that
--   <tt>b1 &amp;&amp; b2 = b3</tt>
class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3

-- | value-level reflection function for the <a>And</a> type-level relation
(&&) :: And b1 b2 b3 => b1 -> b2 -> b3

-- | Or type-level relation. <tt>Or b1 b2 b3</tt> establishes that <tt>b1
--   || b2 = b3</tt>
class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3

-- | value-level reflection function for the <a>Or</a> type-level relation
(||) :: Or b1 b2 b3 => b1 -> b2 -> b3

-- | Exclusive or type-level relation. <tt>Xor b1 b2 b3</tt> establishes
--   that <tt>xor b1 b2 = b3</tt>
class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3

-- | value-level reflection function for the <a>Xor</a> type-level relation
xor :: Xor b1 b2 b3 => b1 -> b2 -> b3

-- | Implication type-level relation. <tt>Imp b1 b2 b3</tt> establishes
--   that <tt>b1 =&gt;b2 = b3</tt>
class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3

-- | value-level reflection function for the Imp type-level relation
imp :: Imp b1 b2 b3 => b1 -> b2 -> b3

-- | Boolean equality type-level relation
class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3

-- | value-level reflection function for the <a>Eq</a> type-level relation
eq :: Eq b1 b2 b3 => b1 -> b2 -> b3
instance Typeable True
instance Typeable False
instance Eq True True True
instance Eq True False False
instance Eq False True False
instance Eq False False True
instance Imp True True True
instance Imp True False False
instance Imp False True True
instance Imp False False True
instance Xor True True False
instance Xor True False True
instance Xor False True True
instance Xor False False False
instance Or True True True
instance Or True False True
instance Or False True True
instance Or False False False
instance And True True True
instance And True False False
instance And False True False
instance And False False False
instance Not True False
instance Not False True
instance BoolI False
instance BoolI True
instance BoolI b => Bool b
instance Show False
instance Show True


-- | Type-level numerical operations and its value-level reflection
--   functions.
module Data.TypeLevel.Num.Ops

-- | Successor type-level relation. <tt>Succ x y</tt> establishes that
--   <tt>succ x = y</tt>.
class (Nat x, Pos y) => Succ x y | x -> y, y -> x

-- | value-level reflection function for the <a>Succ</a> type-level
--   relation
succ :: Succ x y => x -> y

-- | Predecessor type-level relation. <tt>Pred x y</tt> establishes that
--   <tt>pred x = y</tt>.
class (Pos x, Nat y) => Pred x y | x -> y, y -> x

-- | value-level reflection function for the <a>Pred</a> type-level
--   relation
pred :: Pred x y => x -> y

-- | Addition type-level relation. <tt>Add x y z</tt> establishes that
--   <tt>x + y = z</tt>.
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x

-- | value-level reflection function for the <a>Add</a> type-level relation
(+) :: Add x y z => x -> y -> z

-- | Subtraction type-level relation. <tt>Sub x y z</tt> establishes that
--   <tt>x - y = z</tt>
class Sub x y z | x y -> z, z x -> y, z y -> x

-- | value-level reflection function for the <a>Sub</a> type-level relation
(-) :: Sub x y z => x -> y -> z

-- | Multiplication type-level relation. <tt>Mul x y z</tt> establishes
--   that <tt>x * y = z</tt>. Note it isn't relational (i.e. its inverse
--   cannot be used for division, however, even if it could, the resulting
--   division would only work for zero-remainder divisions)
class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z

-- | value-level reflection function for the multiplication type-level
--   relation
(*) :: Mul x y z => x -> y -> z

-- | Division type-level relation. Remainder-discarding version of
--   <a>DivMod</a>. Note it is not relational (due to DivMod not being
--   relational)
class Div x y z | x y -> z, x z -> y, y z -> x

-- | value-level reflection function for the <a>Div</a> type-level relation
div :: Div x y z => x -> y -> z

-- | Remainder of division, type-level relation. <tt>Mod x y r</tt>
--   establishes that <tt>r</tt> is the reminder of dividing <tt>x</tt> by
--   <tt>y</tt>.
class Mod x y r | x y -> r

-- | value-level reflection function for the <a>Mod</a> type-level relation
mod :: Mod x y r => x -> y -> r

-- | Division and Remainder type-level relation. <tt>DivMod x y q r</tt>
--   establishes that <tt>x<i>y = q + r</i>y</tt> Note it is not relational
--   (i.e. its inverse cannot be used for multiplication).
class (Nat x, Pos y) => DivMod x y q r | x y -> q r

-- | value-level reflection function for the <a>DivMod</a> type-level
--   relation
divMod :: DivMod x y q r => x -> y -> (q, r)

-- | Is-divisible-by type-level assertion. e.g <tt>IsDivBy d x</tt>
--   establishes that <tt>x</tt> is divisible by <tt>d</tt>.
class (Pos d, Nat x) => IsDivBy d x

-- | value-level reflection function for IsDivBy
isDivBy :: IsDivBy d x => d -> x

-- | Multiplication by 10 type-level relation (based on <a>DivMod10</a>).
--   <tt>Mul10 x y</tt> establishes that <tt>10 * x = y</tt>.
class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x

-- | value-level reflection function for <a>Mul10</a>
mul10 :: Mul10 x q => x -> q

-- | Division by 10 type-level relation (based on DivMod10)
class (Nat x, Nat q) => Div10 x q | x -> q, q -> x

-- | value-level reflection function for Mul10
div10 :: Div10 x q => x -> q

-- | Division by 10 and Remainer type-level relation (similar to
--   <a>DivMod</a>).
--   
--   This operation is much faster than DivMod. Furthermore, it is the
--   general, non-structural, constructor/deconstructor since it splits a
--   decimal numeral into its initial digits and last digit. Thus, it
--   allows to inspect the structure of a number and is normally used to
--   create type-level operations.
--   
--   Note that contrary to <a>DivMod</a>, <a>DivMod10</a> is relational (it
--   can be used to multiply by 10)
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l

-- | value-level reflection function for DivMod10
divMod10 :: DivMod10 x q r => x -> (q, r)

-- | Exponentation type-level relation. <tt>ExpBase b e r</tt> establishes
--   that <tt>b^e = r</tt> Note it is not relational (i.e. it cannot be
--   used to express logarithms)
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r

-- | value-level reflection function for the ExpBase type-level relation
(^) :: ExpBase b e r => b -> e -> r
class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> e

-- | value-level reflection function for LogBase
logBase :: LogBaseF b x e f => b -> x -> e

-- | Version of LogBase which also outputs if the logarithm calculated was
--   exact. f indicates if the resulting logarithm has no fractional part
--   (i.e. tells if the result provided is exact)
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) => LogBaseF b x e f | b x -> e f

-- | value-level reflection function for LogBaseF
logBaseF :: LogBaseF b x e f => b -> x -> (e, f)

-- | Assert that a number (<tt>x</tt>) can be expressed as the power of
--   another one (<tt>b</tt>) (i.e. the fractional part of <tt>log_base_b x
--   = 0</tt>, or, in a different way, <tt>exists y . b^y = x</tt>).
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x
isPowOf :: IsPowOf b x => b -> x -> ()

-- | Base-10 Exponentiation type-level relation
class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x

-- | value-level reflection function for Exp10
exp10 :: Exp10 x y => x -> y

-- | Base-10 logarithm type-level relation Note it is not relational
--   (cannot be used to express Exponentation to 10) However, it works with
--   any positive numeral (not just powers of 10)
class (Pos x, Nat y) => Log10 x y | x -> y

-- | value-level reflection function for <a>Log10</a>
log10 :: Log10 x y => x -> y

-- | Trichotomy type-level relation. 'Trich x y r' establishes the relation
--   (<tt>r</tt>) between <tt>x</tt> and <tt>y</tt>. The obtained relation
--   (<tt>r</tt>) Can be <a>LT</a> (if <tt>x</tt> is lower than
--   <tt>y</tt>), <a>EQ</a> (if <tt>x</tt> equals <tt>y</tt>) or <a>GT</a>
--   (if <tt>x</tt> is greater than <tt>y</tt>)
class (Nat x, Nat y) => Trich x y r | x y -> r

-- | value-level reflection function for the comparison type-level
--   assertion
trich :: Trich x y r => z -> x -> r

-- | Lower than
data LT

-- | Equal
data EQ

-- | Greater than
data GT

-- | Equality abbreviated type-level assertion
class (:==:) x y

-- | Greater-than abbreviated type-level assertion
class (:>:) x y

-- | Lower-than abbreviated type-level assertion
class (:<:) x y

-- | Greater-than or equal abbreviated type-level assertion
class (:>=:) x y

-- | Lower-than or equal abbreviated type-level assertion
class (:<=:) x y

-- | value-level reflection function for the equality abbreviated
--   type-level assertion
(==) :: x :==: y => x -> y -> ()

-- | value-level reflection function for the equality abbreviated
--   type-level assertion
(>) :: x :>: y => x -> y -> ()

-- | value-level reflection function for the lower-than abbreviated
--   type-level assertion
(<) :: x :<: y => x -> y -> ()

-- | value-level reflection function for the greater-than or equal
--   abbreviated type-level assertion
(>=) :: x :>=: y => x -> y -> ()

-- | value-level reflection function for the lower-than or equal
--   abbreviated type-level assertion
(<=) :: x :<=: y => x -> y -> ()

-- | Maximum type-level relation
class Max x y z | x y -> z

-- | value-level reflection function for the maximum type-level relation
max :: Max x y z => x -> y -> z

-- | Minimum type-level relation
class Min x y z | x y -> z

-- | value-level reflection function for the minimum type-level relation
min :: Min x y z => x -> y -> z

-- | Greatest Common Divisor type-level relation
class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd

-- | value-level reflection function for the GCD type-level relation
gcd :: GCD x y z => x -> y -> z
instance Pos x => IsZero (x :* d) False
instance IsZero D9 False
instance IsZero D8 False
instance IsZero D7 False
instance IsZero D6 False
instance IsZero D5 False
instance IsZero D4 False
instance IsZero D3 False
instance IsZero D2 False
instance IsZero D1 False
instance IsZero D0 True
instance (Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd
instance Nat x => GCD' x x False EQ x
instance (Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd
instance Nat x => GCD' x D0 True cmp D0
instance (Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd) => GCD x y gcd
instance (Max' y x b z, Trich x y b) => Min x y z
instance (Max' x y b z, Trich x y b) => Max x y z
instance Max' x y GT x
instance Max' x y EQ y
instance Max' x y LT y
instance (Succ x' x, Trich x' y LT) => x :<=: y
instance (Succ x x', Trich x' y GT) => x :>=: y
instance Trich x y LT => x :<: y
instance Trich x y GT => x :>: y
instance Trich x y EQ => x :==: y
instance CS LT r LT
instance CS GT r GT
instance CS EQ r r
instance (Pos (xi :* xl), Pos (yi :* yl), Trich xl yl rl, Trich xi yi ri, CS ri rl r) => Trich (xi :* xl) (yi :* yl) r
instance Pos (yi :* yl) => Trich (yi :* yl) D9 GT
instance Pos (yi :* yl) => Trich D9 (yi :* yl) LT
instance Trich D9 D9 EQ
instance Trich D9 D8 GT
instance Trich D9 D7 GT
instance Trich D9 D6 GT
instance Trich D9 D5 GT
instance Trich D9 D4 GT
instance Trich D9 D3 GT
instance Trich D9 D2 GT
instance Trich D9 D1 GT
instance Trich D9 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D8 GT
instance Pos (yi :* yl) => Trich D8 (yi :* yl) LT
instance Trich D8 D9 LT
instance Trich D8 D8 EQ
instance Trich D8 D7 GT
instance Trich D8 D6 GT
instance Trich D8 D5 GT
instance Trich D8 D4 GT
instance Trich D8 D3 GT
instance Trich D8 D2 GT
instance Trich D8 D1 GT
instance Trich D8 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D7 GT
instance Pos (yi :* yl) => Trich D7 (yi :* yl) LT
instance Trich D7 D9 LT
instance Trich D7 D8 LT
instance Trich D7 D7 EQ
instance Trich D7 D6 GT
instance Trich D7 D5 GT
instance Trich D7 D4 GT
instance Trich D7 D3 GT
instance Trich D7 D2 GT
instance Trich D7 D1 GT
instance Trich D7 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D6 GT
instance Pos (yi :* yl) => Trich D6 (yi :* yl) LT
instance Trich D6 D9 LT
instance Trich D6 D8 LT
instance Trich D6 D7 LT
instance Trich D6 D6 EQ
instance Trich D6 D5 GT
instance Trich D6 D4 GT
instance Trich D6 D3 GT
instance Trich D6 D2 GT
instance Trich D6 D1 GT
instance Trich D6 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D5 GT
instance Pos (yi :* yl) => Trich D5 (yi :* yl) LT
instance Trich D5 D9 LT
instance Trich D5 D8 LT
instance Trich D5 D7 LT
instance Trich D5 D6 LT
instance Trich D5 D5 EQ
instance Trich D5 D4 GT
instance Trich D5 D3 GT
instance Trich D5 D2 GT
instance Trich D5 D1 GT
instance Trich D5 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D4 GT
instance Pos (yi :* yl) => Trich D4 (yi :* yl) LT
instance Trich D4 D9 LT
instance Trich D4 D8 LT
instance Trich D4 D7 LT
instance Trich D4 D6 LT
instance Trich D4 D5 LT
instance Trich D4 D4 EQ
instance Trich D4 D3 GT
instance Trich D4 D2 GT
instance Trich D4 D1 GT
instance Trich D4 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D3 GT
instance Pos (yi :* yl) => Trich D3 (yi :* yl) LT
instance Trich D3 D9 LT
instance Trich D3 D8 LT
instance Trich D3 D7 LT
instance Trich D3 D6 LT
instance Trich D3 D5 LT
instance Trich D3 D4 LT
instance Trich D3 D3 EQ
instance Trich D3 D2 GT
instance Trich D3 D1 GT
instance Trich D3 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D2 GT
instance Pos (yi :* yl) => Trich D2 (yi :* yl) LT
instance Trich D2 D9 LT
instance Trich D2 D8 LT
instance Trich D2 D7 LT
instance Trich D2 D6 LT
instance Trich D2 D5 LT
instance Trich D2 D4 LT
instance Trich D2 D3 LT
instance Trich D2 D2 EQ
instance Trich D2 D1 GT
instance Trich D2 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D1 GT
instance Pos (yi :* yl) => Trich D1 (yi :* yl) LT
instance Trich D1 D9 LT
instance Trich D1 D8 LT
instance Trich D1 D7 LT
instance Trich D1 D6 LT
instance Trich D1 D5 LT
instance Trich D1 D4 LT
instance Trich D1 D3 LT
instance Trich D1 D2 LT
instance Trich D1 D1 EQ
instance Trich D1 D0 GT
instance Pos (yi :* yl) => Trich (yi :* yl) D0 GT
instance Pos (yi :* yl) => Trich D0 (yi :* yl) LT
instance Trich D0 D9 LT
instance Trich D0 D8 LT
instance Trich D0 D7 LT
instance Trich D0 D6 LT
instance Trich D0 D5 LT
instance Trich D0 D4 LT
instance Trich D0 D3 LT
instance Trich D0 D2 LT
instance Trich D0 D1 LT
instance Trich D0 D0 EQ
instance (Pos (xi :* xl), Pred y y', Log10 xi y') => Log10 (xi :* xl) y
instance Log10 D9 D0
instance Log10 D8 D0
instance Log10 D7 D0
instance Log10 D6 D0
instance Log10 D5 D0
instance Log10 D4 D0
instance Log10 D3 D0
instance Log10 D2 D0
instance Log10 D1 D0
instance (Pred (xi :* xl) x', Exp10 x' (((((((((y :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)) => Exp10 (xi :* xl) ((((((((((y :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D9 (((((((((D1 :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D8 ((((((((D1 :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D7 (((((((D1 :* D0) :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D6 ((((((D1 :* D0) :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D5 (((((D1 :* D0) :* D0) :* D0) :* D0) :* D0)
instance Exp10 D4 ((((D1 :* D0) :* D0) :* D0) :* D0)
instance Exp10 D3 (((D1 :* D0) :* D0) :* D0)
instance Exp10 D2 ((D1 :* D0) :* D0)
instance Exp10 D1 (D1 :* D0)
instance Exp10 D0 D1
instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) => IsPowOf' b x GT
instance (Pos b, b :>=: D2) => IsPowOf' b b EQ
instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ
instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
instance LogBaseF b x e f => LogBase b x e
instance (Nat b, Pos (ei :* el), Nat r, Mul b r r', Pred (ei :* el) e', ExpBase b e' r) => ExpBase b (ei :* el) r'
instance (Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'
instance (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'
instance (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'
instance (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'
instance (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'
instance (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'
instance (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'
instance Mul b b r => ExpBase b D2 r
instance Nat b => ExpBase b D1 b
instance Nat b => ExpBase b D0 D1
instance DivMod x d q D0 => IsDivBy d x
instance DivMod10 x q r => Div10 x q
instance (Nat (x :* l), Nat ((x :* l) :* l')) => DivMod10 ((x :* l) :* l') (x :* l) l'
instance Nat (D9 :* l) => DivMod10 (D9 :* l) D9 l
instance Nat (D8 :* l) => DivMod10 (D8 :* l) D8 l
instance Nat (D7 :* l) => DivMod10 (D7 :* l) D7 l
instance Nat (D6 :* l) => DivMod10 (D6 :* l) D6 l
instance Nat (D5 :* l) => DivMod10 (D5 :* l) D5 l
instance Nat (D4 :* l) => DivMod10 (D4 :* l) D4 l
instance Nat (D3 :* l) => DivMod10 (D3 :* l) D3 l
instance Nat (D2 :* l) => DivMod10 (D2 :* l) D2 l
instance Nat (D1 :* l) => DivMod10 (D1 :* l) D1 l
instance DivMod10 D9 D0 D9
instance DivMod10 D8 D0 D8
instance DivMod10 D7 D0 D7
instance DivMod10 D6 D0 D6
instance DivMod10 D5 D0 D5
instance DivMod10 D4 D0 D4
instance DivMod10 D3 D0 D3
instance DivMod10 D2 D0 D2
instance DivMod10 D1 D0 D1
instance DivMod10 D0 D0 D0
instance DivMod10 x q D0 => Mul10 q x
instance DivMod x y q r => Mod x y r
instance DivMod x y q r => Div x y q
instance (Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivMod' x y q r GT
instance (Nat x, Pos y) => DivMod' x y D1 D0 EQ
instance (Nat x, Pos y) => DivMod' x y D0 x LT
instance (Pos y, Trich x y cmp, DivMod' x y q r cmp) => DivMod x y q r
instance (Pos (xi :* xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, Add dy z10 z') => Mul (xi :* xl) y z'
instance (Add z y z', Mul D8 y z) => Mul D9 y z'
instance (Add z y z', Mul D7 y z) => Mul D8 y z'
instance (Add z y z', Mul D6 y z) => Mul D7 y z'
instance (Add z y z', Mul D5 y z) => Mul D6 y z'
instance (Add z y z', Mul D4 y z) => Mul D5 y z'
instance (Add z y z', Mul D3 y z) => Mul D4 y z'
instance (Add z y z', Mul D2 y z) => Mul D3 y z'
instance Add y y z => Mul D2 y z
instance Nat y => Mul D1 y y
instance Nat y => Mul D0 y D0
instance Add x y z => Sub z y x
instance (Add' x y z, Add' y x z) => Add x y z
instance (Pos (xi :* xl), Nat z, Add' xi yi zi, DivMod10 y yi yl, Add' xl (zi :* yl) z) => Add' (xi :* xl) y z
instance (Succ z z', Add' D8 y z) => Add' D9 y z'
instance (Succ z z', Add' D7 y z) => Add' D8 y z'
instance (Succ z z', Add' D6 y z) => Add' D7 y z'
instance (Succ z z', Add' D5 y z) => Add' D6 y z'
instance (Succ z z', Add' D4 y z) => Add' D5 y z'
instance (Succ z z', Add' D3 y z) => Add' D4 y z'
instance (Succ z z', Add' D2 y z) => Add' D3 y z'
instance (Succ z z', Add' D1 y z) => Add' D2 y z'
instance Succ y z => Add' D1 y z
instance Nat y => Add' D0 y y
instance Succ x y => Pred y x
instance Succ xi yi => Succ' xi D9 yi D0 False
instance Succ' xi D8 xi D9 False
instance Succ' xi D7 xi D8 False
instance Succ' xi D6 xi D7 False
instance Succ' xi D5 xi D6 False
instance Succ' xi D4 xi D5 False
instance Succ' xi D3 xi D4 False
instance Succ' xi D2 xi D3 False
instance Succ' xi D1 xi D2 False
instance Succ' xi D0 xi D1 False
instance Failure (PredecessorOfZeroError x) => Succ' (x, x) (x, x) D0 D0 True
instance (Pos y, IsZero y yz, DivMod10 x xi xl, Succ' xi xl yi yl yz, DivMod10 y yi yl) => Succ x y


-- | This module is a wrapper for all the publicly usable numerical types
--   and functions of the type-level library.
--   
--   Here is a tutorial on type-level numerals and how to use them to
--   implement numerically-parameterized vectors:
--   <a>http://www.ict.kth.se/org/ict/ecs/sam/projects/forsyde/www/files/tutorial/tutorial.html#FSVec</a>
module Data.TypeLevel.Num


-- | This module is a wrapper for all the publicly usable types and
--   functions of the type-level library.
module Data.TypeLevel
