type-level-0.2: Type-level programming library Source code Contents Index

Data.TypeLevel.Num.Reps Portability non-portable (TypeOperators) Stability experimental Maintainer alfonso.acosta@gmail.com

Contents Decimal representation

Description

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

Synopsis

data D0 data D1 data D2 data D3 data D4 data D5 data D6 data D7 data D8 data D9 data a :* b = a :* b

Decimal representation

data D0 Source

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