Copyright	(c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and KTH's SAM group
License	BSD-style (see the file LICENSE)
Maintainer	alfonso.acosta@gmail.com
Stability	experimental
Portability	non-portable (TypeOperators)
Safe Haskell	None
Language	Haskell98

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 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

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

data D2 Source

Decimal digit two

Instances

Show D2 Source
Lift D2 Source
Log10 D2 D0 Source
Trich D9 D2 GT Source
Trich D8 D2 GT Source
Trich D7 D2 GT Source
Trich D6 D2 GT Source
Trich D5 D2 GT Source
Trich D4 D2 GT Source
Trich D3 D2 GT Source
Trich D2 D9 LT Source
Trich D2 D8 LT Source
Trich D2 D7 LT Source
Trich D2 D6 LT Source
Trich D2 D5 LT Source
Trich D2 D4 LT Source
Trich D2 D3 LT Source
Trich D2 D2 EQ Source
Trich D2 D1 GT Source
Trich D2 D0 GT Source
Trich D1 D2 LT Source
Trich D0 D2 LT Source
Mul b b r => ExpBase b D2 r Source
DivMod10 D2 D0 D2 Source
Add y y z => Mul D2 y z Source
Exp10 D2 ((:) ((:) D1 D0) D0) Source
Pos ((:) yi yl) => Trich D2 ((:) yi yl) LT Source
Pos ((:) yi yl) => Trich ((:) yi yl) D2 GT Source
Nat ((:) D2 l) => DivMod10 ((:) D2 l) D2 l Source

data D3 Source

Decimal digit three

Instances

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

data D4 Source

Decimal digit four

Instances

Show D4 Source
Lift D4 Source
Log10 D4 D0 Source
Trich D9 D4 GT Source
Trich D8 D4 GT Source
Trich D7 D4 GT Source
Trich D6 D4 GT Source
Trich D5 D4 GT Source
Trich D4 D9 LT Source
Trich D4 D8 LT Source
Trich D4 D7 LT Source
Trich D4 D6 LT Source
Trich D4 D5 LT Source
Trich D4 D4 EQ Source
Trich D4 D3 GT Source
Trich D4 D2 GT Source
Trich D4 D1 GT Source
Trich D4 D0 GT Source
Trich D3 D4 LT Source
Trich D2 D4 LT Source
Trich D1 D4 LT Source
Trich D0 D4 LT Source
(Mul r b r', ExpBase b D3 r) => ExpBase b D4 r' Source
DivMod10 D4 D0 D4 Source
(Add z y z', Mul D3 y z) => Mul D4 y z' Source
Exp10 D4 ((:) ((:) ((:) ((:) D1 D0) D0) D0) D0) Source
Pos ((:) yi yl) => Trich D4 ((:) yi yl) LT Source
Pos ((:) yi yl) => Trich ((:) yi yl) D4 GT Source
Nat ((:) D4 l) => DivMod10 ((:) D4 l) D4 l Source

data D5 Source

Decimal digit five

Instances

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

data D6 Source

Decimal digit six

Instances

Show D6 Source
Lift D6 Source
Log10 D6 D0 Source
Trich D9 D6 GT Source
Trich D8 D6 GT Source
Trich D7 D6 GT Source
Trich D6 D9 LT Source
Trich D6 D8 LT Source
Trich D6 D7 LT Source
Trich D6 D6 EQ Source
Trich D6 D5 GT Source
Trich D6 D4 GT Source
Trich D6 D3 GT Source
Trich D6 D2 GT Source
Trich D6 D1 GT Source
Trich D6 D0 GT Source
Trich D5 D6 LT Source
Trich D4 D6 LT Source
Trich D3 D6 LT Source
Trich D2 D6 LT Source
Trich D1 D6 LT Source
Trich D0 D6 LT Source
(Mul r b r', ExpBase b D5 r) => ExpBase b D6 r' Source
DivMod10 D6 D0 D6 Source
(Add z y z', Mul D5 y z) => Mul D6 y z' Source
Exp10 D6 ((:) ((:) ((:) ((:) ((:) ((:) D1 D0) D0) D0) D0) D0) D0) Source
Pos ((:) yi yl) => Trich D6 ((:) yi yl) LT Source
Pos ((:) yi yl) => Trich ((:) yi yl) D6 GT Source
Nat ((:) D6 l) => DivMod10 ((:) D6 l) D6 l Source

data D7 Source

Decimal digit seven

Instances

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

data D8 Source

Decimal digit eight

Instances

Show D8 Source
Lift D8 Source
Log10 D8 D0 Source
Trich D9 D8 GT Source
Trich D8 D9 LT Source
Trich D8 D8 EQ Source
Trich D8 D7 GT Source
Trich D8 D6 GT Source
Trich D8 D5 GT Source
Trich D8 D4 GT Source
Trich D8 D3 GT Source
Trich D8 D2 GT Source
Trich D8 D1 GT Source
Trich D8 D0 GT Source
Trich D7 D8 LT Source
Trich D6 D8 LT Source
Trich D5 D8 LT Source
Trich D4 D8 LT Source
Trich D3 D8 LT Source
Trich D2 D8 LT Source
Trich D1 D8 LT Source
Trich D0 D8 LT Source
(Mul r b r', ExpBase b D7 r) => ExpBase b D8 r' Source
DivMod10 D8 D0 D8 Source
(Add z y z', Mul D7 y z) => Mul D8 y z' Source
Exp10 D8 ((:) ((:) ((:) ((:) ((:) ((:) ((:) ((:) D1 D0) D0) D0) D0) D0) D0) D0) D0) Source
Pos ((:) yi yl) => Trich D8 ((:) yi yl) LT Source
Pos ((:) yi yl) => Trich ((:) yi yl) D8 GT Source
Nat ((:) D8 l) => DivMod10 ((:) D8 l) D8 l Source

data D9 Source

Decimal digit nine

Instances

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

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

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