Portability	non-portable (TypeOperators)
Stability	experimental
Maintainer	[email protected]

Data.TypeLevel.Num.Reps

Contents

Decimal representation

Description

Type-level numerical representations. Currently, only decimals are supported.

Synopsis

Decimal representation

data D0 Source

Decimal digit zero

Instances

Show D0
Typeable D0
Lift D0
NatI D0
IsZero D0 True
Log10 D9 D0
Log10 D8 D0
Log10 D7 D0
Log10 D6 D0
Log10 D5 D0
Log10 D4 D0
Log10 D3 D0
Log10 D2 D0
Log10 D1 D0
Exp10 D0 D1
Trich D9 D0 GT
Trich D8 D0 GT
Trich D7 D0 GT
Trich D6 D0 GT
Trich D5 D0 GT
Trich D4 D0 GT
Trich D3 D0 GT
Trich D2 D0 GT
Trich D1 D0 GT
Trich D0 D9 LT
Trich D0 D8 LT
Trich D0 D7 LT
Trich D0 D6 LT
Trich D0 D5 LT
Trich D0 D4 LT
Trich D0 D3 LT
Trich D0 D2 LT
Trich D0 D1 LT
Trich D0 D0 EQ
Nat b => ExpBase b D0 D1
DivMod10 D9 D0 D9
DivMod10 D8 D0 D8
DivMod10 D7 D0 D7
DivMod10 D6 D0 D6
DivMod10 D5 D0 D5
DivMod10 D4 D0 D4
DivMod10 D3 D0 D3
DivMod10 D2 D0 D2
DivMod10 D1 D0 D1
DivMod10 D0 D0 D0
Nat y => Mul D0 y D0
Nat y => Add' D0 y y
Nat x => GCD' x D0 True cmp D0
(Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
(Nat x, Pos y) => DivMod' x y D1 D0 EQ
(Nat x, Pos y) => DivMod' x y D0 x LT
Succ xi yi => Succ' xi D9 yi D0 False
Succ' xi D0 xi D1 False
Exp10 D9 (:* (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D8 (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D7 (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0)
Exp10 D6 (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0)
Exp10 D5 (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0)
Exp10 D4 (:* (:* (:* (:* D1 D0) D0) D0) D0)
Exp10 D3 (:* (:* (:* D1 D0) D0) D0)
Exp10 D2 (:* (:* D1 D0) D0)
Exp10 D1 (:* D1 D0)
Pos (:* yi yl) => Trich D0 (:* yi yl) LT
PosI x => PosI (:* x D0)
PosI x => NatI (:* x D0)
Pos (:* yi yl) => Trich (:* yi yl) D0 GT
(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)
Failure (PredecessorOfZeroError x) => Succ' (x, x) (x, x) D0 D0 True

data D1 Source

Decimal digit one

Instances

Show D1
Typeable D1
Lift D1
PosI D1
NatI D1
IsZero D1 False
Log10 D1 D0
Exp10 D0 D1
Trich D9 D1 GT
Trich D8 D1 GT
Trich D7 D1 GT
Trich D6 D1 GT
Trich D5 D1 GT
Trich D4 D1 GT
Trich D3 D1 GT
Trich D2 D1 GT
Trich D1 D9 LT
Trich D1 D8 LT
Trich D1 D7 LT
Trich D1 D6 LT
Trich D1 D5 LT
Trich D1 D4 LT
Trich D1 D3 LT
Trich D1 D2 LT
Trich D1 D1 EQ
Trich D1 D0 GT
Trich D0 D1 LT
Nat b => ExpBase b D1 b
Nat b => ExpBase b D0 D1
DivMod10 D1 D0 D1
Nat y => Mul D1 y y
Succ y z => Add' D1 y z
(Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ
(Nat x, Pos y) => DivMod' x y D1 D0 EQ
Succ' xi D1 xi D2 False
Succ' xi D0 xi D1 False
Exp10 D9 (:* (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D8 (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D7 (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0)
Exp10 D6 (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0)
Exp10 D5 (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0)
Exp10 D4 (:* (:* (:* (:* D1 D0) D0) D0) D0)
Exp10 D3 (:* (:* (:* D1 D0) D0) D0)
Exp10 D2 (:* (:* D1 D0) D0)
Exp10 D1 (:* D1 D0)
Pos (:* yi yl) => Trich D1 (:* yi yl) LT
PosI x => PosI (:* x D1)
PosI x => NatI (:* x D1)
Pos (:* yi yl) => Trich (:* yi yl) D1 GT
Nat (:* D1 l) => DivMod10 (:* D1 l) D1 l

data D2 Source

Decimal digit two

Instances

Show D2
Typeable D2
Lift D2
PosI D2
NatI D2
IsZero D2 False
Log10 D2 D0
Trich D9 D2 GT
Trich D8 D2 GT
Trich D7 D2 GT
Trich D6 D2 GT
Trich D5 D2 GT
Trich D4 D2 GT
Trich D3 D2 GT
Trich D2 D9 LT
Trich D2 D8 LT
Trich D2 D7 LT
Trich D2 D6 LT
Trich D2 D5 LT
Trich D2 D4 LT
Trich D2 D3 LT
Trich D2 D2 EQ
Trich D2 D1 GT
Trich D2 D0 GT
Trich D1 D2 LT
Trich D0 D2 LT
Mul b b r => ExpBase b D2 r
DivMod10 D2 D0 D2
Add y y z => Mul D2 y z
(Succ z z', Add' D1 y z) => Add' D2 y z'
Succ' xi D2 xi D3 False
Succ' xi D1 xi D2 False
Exp10 D2 (:* (:* D1 D0) D0)
Pos (:* yi yl) => Trich D2 (:* yi yl) LT
PosI x => PosI (:* x D2)
PosI x => NatI (:* x D2)
Pos (:* yi yl) => Trich (:* yi yl) D2 GT
Nat (:* D2 l) => DivMod10 (:* D2 l) D2 l

data D3 Source

Decimal digit three

Instances

Show D3
Typeable D3
Lift D3
PosI D3
NatI D3
IsZero D3 False
Log10 D3 D0
Trich D9 D3 GT
Trich D8 D3 GT
Trich D7 D3 GT
Trich D6 D3 GT
Trich D5 D3 GT
Trich D4 D3 GT
Trich D3 D9 LT
Trich D3 D8 LT
Trich D3 D7 LT
Trich D3 D6 LT
Trich D3 D5 LT
Trich D3 D4 LT
Trich D3 D3 EQ
Trich D3 D2 GT
Trich D3 D1 GT
Trich D3 D0 GT
Trich D2 D3 LT
Trich D1 D3 LT
Trich D0 D3 LT
(Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'
DivMod10 D3 D0 D3
(Add z y z', Mul D2 y z) => Mul D3 y z'
(Succ z z', Add' D2 y z) => Add' D3 y z'
Succ' xi D3 xi D4 False
Succ' xi D2 xi D3 False
Exp10 D3 (:* (:* (:* D1 D0) D0) D0)
Pos (:* yi yl) => Trich D3 (:* yi yl) LT
PosI x => PosI (:* x D3)
PosI x => NatI (:* x D3)
Pos (:* yi yl) => Trich (:* yi yl) D3 GT
Nat (:* D3 l) => DivMod10 (:* D3 l) D3 l

data D4 Source

Decimal digit four

Instances

Show D4
Typeable D4
Lift D4
PosI D4
NatI D4
IsZero D4 False
Log10 D4 D0
Trich D9 D4 GT
Trich D8 D4 GT
Trich D7 D4 GT
Trich D6 D4 GT
Trich D5 D4 GT
Trich D4 D9 LT
Trich D4 D8 LT
Trich D4 D7 LT
Trich D4 D6 LT
Trich D4 D5 LT
Trich D4 D4 EQ
Trich D4 D3 GT
Trich D4 D2 GT
Trich D4 D1 GT
Trich D4 D0 GT
Trich D3 D4 LT
Trich D2 D4 LT
Trich D1 D4 LT
Trich D0 D4 LT
(Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'
DivMod10 D4 D0 D4
(Add z y z', Mul D3 y z) => Mul D4 y z'
(Succ z z', Add' D3 y z) => Add' D4 y z'
Succ' xi D4 xi D5 False
Succ' xi D3 xi D4 False
Exp10 D4 (:* (:* (:* (:* D1 D0) D0) D0) D0)
Pos (:* yi yl) => Trich D4 (:* yi yl) LT
PosI x => PosI (:* x D4)
PosI x => NatI (:* x D4)
Pos (:* yi yl) => Trich (:* yi yl) D4 GT
Nat (:* D4 l) => DivMod10 (:* D4 l) D4 l

data D5 Source

Decimal digit five

Instances

Show D5
Typeable D5
Lift D5
PosI D5
NatI D5
IsZero D5 False
Log10 D5 D0
Trich D9 D5 GT
Trich D8 D5 GT
Trich D7 D5 GT
Trich D6 D5 GT
Trich D5 D9 LT
Trich D5 D8 LT
Trich D5 D7 LT
Trich D5 D6 LT
Trich D5 D5 EQ
Trich D5 D4 GT
Trich D5 D3 GT
Trich D5 D2 GT
Trich D5 D1 GT
Trich D5 D0 GT
Trich D4 D5 LT
Trich D3 D5 LT
Trich D2 D5 LT
Trich D1 D5 LT
Trich D0 D5 LT
(Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'
DivMod10 D5 D0 D5
(Add z y z', Mul D4 y z) => Mul D5 y z'
(Succ z z', Add' D4 y z) => Add' D5 y z'
Succ' xi D5 xi D6 False
Succ' xi D4 xi D5 False
Exp10 D5 (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0)
Pos (:* yi yl) => Trich D5 (:* yi yl) LT
PosI x => PosI (:* x D5)
PosI x => NatI (:* x D5)
Pos (:* yi yl) => Trich (:* yi yl) D5 GT
Nat (:* D5 l) => DivMod10 (:* D5 l) D5 l

data D6 Source

Decimal digit six

Instances

Show D6
Typeable D6
Lift D6
PosI D6
NatI D6
IsZero D6 False
Log10 D6 D0
Trich D9 D6 GT
Trich D8 D6 GT
Trich D7 D6 GT
Trich D6 D9 LT
Trich D6 D8 LT
Trich D6 D7 LT
Trich D6 D6 EQ
Trich D6 D5 GT
Trich D6 D4 GT
Trich D6 D3 GT
Trich D6 D2 GT
Trich D6 D1 GT
Trich D6 D0 GT
Trich D5 D6 LT
Trich D4 D6 LT
Trich D3 D6 LT
Trich D2 D6 LT
Trich D1 D6 LT
Trich D0 D6 LT
(Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'
DivMod10 D6 D0 D6
(Add z y z', Mul D5 y z) => Mul D6 y z'
(Succ z z', Add' D5 y z) => Add' D6 y z'
Succ' xi D6 xi D7 False
Succ' xi D5 xi D6 False
Exp10 D6 (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0)
Pos (:* yi yl) => Trich D6 (:* yi yl) LT
PosI x => PosI (:* x D6)
PosI x => NatI (:* x D6)
Pos (:* yi yl) => Trich (:* yi yl) D6 GT
Nat (:* D6 l) => DivMod10 (:* D6 l) D6 l

data D7 Source

Decimal digit seven

Instances

Show D7
Typeable D7
Lift D7
PosI D7
NatI D7
IsZero D7 False
Log10 D7 D0
Trich D9 D7 GT
Trich D8 D7 GT
Trich D7 D9 LT
Trich D7 D8 LT
Trich D7 D7 EQ
Trich D7 D6 GT
Trich D7 D5 GT
Trich D7 D4 GT
Trich D7 D3 GT
Trich D7 D2 GT
Trich D7 D1 GT
Trich D7 D0 GT
Trich D6 D7 LT
Trich D5 D7 LT
Trich D4 D7 LT
Trich D3 D7 LT
Trich D2 D7 LT
Trich D1 D7 LT
Trich D0 D7 LT
(Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'
DivMod10 D7 D0 D7
(Add z y z', Mul D6 y z) => Mul D7 y z'
(Succ z z', Add' D6 y z) => Add' D7 y z'
Succ' xi D7 xi D8 False
Succ' xi D6 xi D7 False
Exp10 D7 (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0)
Pos (:* yi yl) => Trich D7 (:* yi yl) LT
PosI x => PosI (:* x D7)
PosI x => NatI (:* x D7)
Pos (:* yi yl) => Trich (:* yi yl) D7 GT
Nat (:* D7 l) => DivMod10 (:* D7 l) D7 l

data D8 Source

Decimal digit eight

Instances

Show D8
Typeable D8
Lift D8
PosI D8
NatI D8
IsZero D8 False
Log10 D8 D0
Trich D9 D8 GT
Trich D8 D9 LT
Trich D8 D8 EQ
Trich D8 D7 GT
Trich D8 D6 GT
Trich D8 D5 GT
Trich D8 D4 GT
Trich D8 D3 GT
Trich D8 D2 GT
Trich D8 D1 GT
Trich D8 D0 GT
Trich D7 D8 LT
Trich D6 D8 LT
Trich D5 D8 LT
Trich D4 D8 LT
Trich D3 D8 LT
Trich D2 D8 LT
Trich D1 D8 LT
Trich D0 D8 LT
(Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'
DivMod10 D8 D0 D8
(Add z y z', Mul D7 y z) => Mul D8 y z'
(Succ z z', Add' D7 y z) => Add' D8 y z'
Succ' xi D8 xi D9 False
Succ' xi D7 xi D8 False
Exp10 D8 (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0)
Pos (:* yi yl) => Trich D8 (:* yi yl) LT
PosI x => PosI (:* x D8)
PosI x => NatI (:* x D8)
Pos (:* yi yl) => Trich (:* yi yl) D8 GT
Nat (:* D8 l) => DivMod10 (:* D8 l) D8 l

data D9 Source

Decimal digit nine

Instances

Show D9
Typeable D9
Lift D9
PosI D9
NatI D9
IsZero D9 False
Log10 D9 D0
Trich D9 D9 EQ
Trich D9 D8 GT
Trich D9 D7 GT
Trich D9 D6 GT
Trich D9 D5 GT
Trich D9 D4 GT
Trich D9 D3 GT
Trich D9 D2 GT
Trich D9 D1 GT
Trich D9 D0 GT
Trich D8 D9 LT
Trich D7 D9 LT
Trich D6 D9 LT
Trich D5 D9 LT
Trich D4 D9 LT
Trich D3 D9 LT
Trich D2 D9 LT
Trich D1 D9 LT
Trich D0 D9 LT
(Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'
DivMod10 D9 D0 D9
(Add z y z', Mul D8 y z) => Mul D9 y z'
(Succ z z', Add' D8 y z) => Add' D9 y z'
Succ xi yi => Succ' xi D9 yi D0 False
Succ' xi D8 xi D9 False
Exp10 D9 (:* (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0) D0)
Pos (:* yi yl) => Trich D9 (:* yi yl) LT
PosI x => PosI (:* x D9)
PosI x => NatI (:* x D9)
Pos (:* yi yl) => Trich (:* yi yl) D9 GT
Nat (:* D9 l) => DivMod10 (:* D9 l) D9 l

data a :* b Source

Connective to glue digits together. For example, D1 :* D0 :* D0 represents the decimal number 100

Constructors

a :* b

Instances

Typeable2 :*
Exp10 D9 (:* (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D8 (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D7 (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0)
Exp10 D6 (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0)
Exp10 D5 (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0)
Exp10 D4 (:* (:* (:* (:* D1 D0) D0) D0) D0)
Exp10 D3 (:* (:* (:* D1 D0) D0) D0)
Exp10 D2 (:* (:* D1 D0) D0)
Exp10 D1 (:* D1 D0)
Pos (:* yi yl) => Trich D9 (:* yi yl) LT
Pos (:* yi yl) => Trich D8 (:* yi yl) LT
Pos (:* yi yl) => Trich D7 (:* yi yl) LT
Pos (:* yi yl) => Trich D6 (:* yi yl) LT
Pos (:* yi yl) => Trich D5 (:* yi yl) LT
Pos (:* yi yl) => Trich D4 (:* yi yl) LT
Pos (:* yi yl) => Trich D3 (:* yi yl) LT
Pos (:* yi yl) => Trich D2 (:* yi yl) LT
Pos (:* yi yl) => Trich D1 (:* yi yl) LT
Pos (:* yi yl) => Trich D0 (:* yi yl) LT
(Nat b, Pos (:* ei el), Nat r, Mul b r r', Pred (:* ei el) e', ExpBase b e' r) => ExpBase b (:* ei el) r'
(Show a, Show b) => Show (:* a b)
(Lift a, Lift b) => Lift (:* a b)
PosI x => PosI (:* x D9)
PosI x => PosI (:* x D8)
PosI x => PosI (:* x D7)
PosI x => PosI (:* x D6)
PosI x => PosI (:* x D5)
PosI x => PosI (:* x D4)
PosI x => PosI (:* x D3)
PosI x => PosI (:* x D2)
PosI x => PosI (:* x D1)
PosI x => PosI (:* x D0)
PosI x => NatI (:* x D9)
PosI x => NatI (:* x D8)
PosI x => NatI (:* x D7)
PosI x => NatI (:* x D6)
PosI x => NatI (:* x D5)
PosI x => NatI (:* x D4)
PosI x => NatI (:* x D3)
PosI x => NatI (:* x D2)
PosI x => NatI (:* x D1)
PosI x => NatI (:* x D0)
Pos x => IsZero (:* x d) False
(Pos (:* xi xl), Pred y y', Log10 xi y') => Log10 (:* xi xl) y
Pos (:* yi yl) => Trich (:* yi yl) D9 GT
Pos (:* yi yl) => Trich (:* yi yl) D8 GT
Pos (:* yi yl) => Trich (:* yi yl) D7 GT
Pos (:* yi yl) => Trich (:* yi yl) D6 GT
Pos (:* yi yl) => Trich (:* yi yl) D5 GT
Pos (:* yi yl) => Trich (:* yi yl) D4 GT
Pos (:* yi yl) => Trich (:* yi yl) D3 GT
Pos (:* yi yl) => Trich (:* yi yl) D2 GT
Pos (:* yi yl) => Trich (:* yi yl) D1 GT
Pos (:* yi yl) => Trich (:* yi yl) D0 GT
Nat (:* D9 l) => DivMod10 (:* D9 l) D9 l
Nat (:* D8 l) => DivMod10 (:* D8 l) D8 l
Nat (:* D7 l) => DivMod10 (:* D7 l) D7 l
Nat (:* D6 l) => DivMod10 (:* D6 l) D6 l
Nat (:* D5 l) => DivMod10 (:* D5 l) D5 l
Nat (:* D4 l) => DivMod10 (:* D4 l) D4 l
Nat (:* D3 l) => DivMod10 (:* D3 l) D3 l
Nat (:* D2 l) => DivMod10 (:* D2 l) D2 l
Nat (:* D1 l) => DivMod10 (:* D1 l) D1 l
(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'
(Pos (:* xi xl), Nat z, Add' xi yi zi, DivMod10 y yi yl, Add' xl (:* zi yl) z) => Add' (:* xi xl) y z
(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)
(Pos (:* xi xl), Pos (:* yi yl), Trich xl yl rl, Trich xi yi ri, CS ri rl r) => Trich (:* xi xl) (:* yi yl) r
(Nat (:* x l), Nat (:* (:* x l) l')) => DivMod10 (:* (:* x l) l') (:* x l) l'