type-level-0.3.0: Type-level programming library

Copyright(c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and KTH's SAM group
LicenseBSD-style (see the file LICENSE)
Maintainer[email protected]
Stabilityexperimental
Portabilitynon-portable (TypeOperators)
Safe HaskellNone
LanguageHaskell98

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 Source 
Lift D0 Source 
Log10 D9 D0 Source 
Log10 D8 D0 Source 
Log10 D7 D0 Source 
Log10 D6 D0 Source 
Log10 D5 D0 Source 
Log10 D4 D0 Source 
Log10 D3 D0 Source 
Log10 D2 D0 Source 
Log10 D1 D0 Source 
Exp10 D0 D1 Source 
Trich D9 D0 GT Source 
Trich D8 D0 GT Source 
Trich D7 D0 GT Source 
Trich D6 D0 GT Source 
Trich D5 D0 GT Source 
Trich D4 D0 GT Source 
Trich D3 D0 GT Source 
Trich D2 D0 GT Source 
Trich D1 D0 GT Source 
Trich D0 D9 LT Source 
Trich D0 D8 LT Source 
Trich D0 D7 LT Source 
Trich D0 D6 LT Source 
Trich D0 D5 LT Source 
Trich D0 D4 LT Source 
Trich D0 D3 LT Source 
Trich D0 D2 LT Source 
Trich D0 D1 LT Source 
Trich D0 D0 EQ Source 
Nat b => ExpBase b D0 D1 Source 
DivMod10 D9 D0 D9 Source 
DivMod10 D8 D0 D8 Source 
DivMod10 D7 D0 D7 Source 
DivMod10 D6 D0 D6 Source 
DivMod10 D5 D0 D5 Source 
DivMod10 D4 D0 D4 Source 
DivMod10 D3 D0 D3 Source 
DivMod10 D2 D0 D2 Source 
DivMod10 D1 D0 D1 Source 
DivMod10 D0 D0 D0 Source 
Nat y => Mul D0 y D0 Source 
Exp10 D9 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) D0) D0) Source 
Exp10 D8 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) D0) Source 
Exp10 D7 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) Source 
Exp10 D6 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) Source 
Exp10 D5 ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) Source 
Exp10 D4 ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) Source 
Exp10 D3 ((:*) ((:*) ((:*) D1 D0) D0) D0) Source 
Exp10 D2 ((:*) ((:*) D1 D0) D0) Source 
Exp10 D1 ((:*) D1 D0) Source 
Pos ((:*) yi yl) => Trich D0 ((:*) yi yl) LT Source 
Pos ((:*) yi yl) => Trich ((:*) yi yl) D0 GT Source 
(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) Source 

data D1 Source

Decimal digit one

Instances

data D2 Source

Decimal digit two

Instances

data D3 Source

Decimal digit three

Instances

data D4 Source

Decimal digit four

Instances

data D5 Source

Decimal digit five

Instances

data D6 Source

Decimal digit six

Instances

data D7 Source

Decimal digit seven

Instances

data D8 Source

Decimal digit eight

Instances

data D9 Source

Decimal digit nine

Instances

data a :* b Source

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

Constructors

a :* b 

Instances

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