type-level-0.2.4: Type-level programming library

Portabilitynon-portable (TypeOperators)
Stabilityexperimental
Maintaineralfonso.acosta@gmail.com

Data.TypeLevel.Num.Reps

Contents

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'