Module

Data.Typelevel.Num

Re-exports from Data.Typelevel.Num.Aliases

#D99

type D99 = D9 :* D9

#D98

type D98 = D9 :* D8

#D97

type D97 = D9 :* D7

#D96

type D96 = D9 :* D6

#D95

type D95 = D9 :* D5

#D94

type D94 = D9 :* D4

#D93

type D93 = D9 :* D3

#D92

type D92 = D9 :* D2

#D91

type D91 = D9 :* D1

#D90

type D90 = D9 :* D0

#D89

type D89 = D8 :* D9

#D88

type D88 = D8 :* D8

#D87

type D87 = D8 :* D7

#D86

type D86 = D8 :* D6

#D85

type D85 = D8 :* D5

#D84

type D84 = D8 :* D4

#D83

type D83 = D8 :* D3

#D82

type D82 = D8 :* D2

#D81

type D81 = D8 :* D1

#D80

type D80 = D8 :* D0

#D79

type D79 = D7 :* D9

#D78

type D78 = D7 :* D8

#D77

type D77 = D7 :* D7

#D76

type D76 = D7 :* D6

#D75

type D75 = D7 :* D5

#D74

type D74 = D7 :* D4

#D73

type D73 = D7 :* D3

#D72

type D72 = D7 :* D2

#D71

type D71 = D7 :* D1

#D70

type D70 = D7 :* D0

#D69

type D69 = D6 :* D9

#D68

type D68 = D6 :* D8

#D67

type D67 = D6 :* D7

#D66

type D66 = D6 :* D6

#D65

type D65 = D6 :* D5

#D64

type D64 = D6 :* D4

#D63

type D63 = D6 :* D3

#D62

type D62 = D6 :* D2

#D61

type D61 = D6 :* D1

#D60

type D60 = D6 :* D0

#D59

type D59 = D5 :* D9

#D58

type D58 = D5 :* D8

#D57

type D57 = D5 :* D7

#D56

type D56 = D5 :* D6

#D55

type D55 = D5 :* D5

#D54

type D54 = D5 :* D4

#D53

type D53 = D5 :* D3

#D52

type D52 = D5 :* D2

#D51

type D51 = D5 :* D1

#D50

type D50 = D5 :* D0

#D49

type D49 = D4 :* D9

#D48

type D48 = D4 :* D8

#D47

type D47 = D4 :* D7

#D46

type D46 = D4 :* D6

#D45

type D45 = D4 :* D5

#D44

type D44 = D4 :* D4

#D43

type D43 = D4 :* D3

#D42

type D42 = D4 :* D2

#D41

type D41 = D4 :* D1

#D40

type D40 = D4 :* D0

#D39

type D39 = D3 :* D9

#D38

type D38 = D3 :* D8

#D37

type D37 = D3 :* D7

#D36

type D36 = D3 :* D6

#D35

type D35 = D3 :* D5

#D34

type D34 = D3 :* D4

#D33

type D33 = D3 :* D3

#D32

type D32 = D3 :* D2

#D31

type D31 = D3 :* D1

#D30

type D30 = D3 :* D0

#D29

type D29 = D2 :* D9

#D28

type D28 = D2 :* D8

#D27

type D27 = D2 :* D7

#D26

type D26 = D2 :* D6

#D25

type D25 = D2 :* D5

#D24

type D24 = D2 :* D4

#D23

type D23 = D2 :* D3

#D22

type D22 = D2 :* D2

#D21

type D21 = D2 :* D1

#D20

type D20 = D2 :* D0

#D19

type D19 = D1 :* D9

#D18

type D18 = D1 :* D8

#D17

type D17 = D1 :* D7

#D16

type D16 = D1 :* D6

#D15

type D15 = D1 :* D5

#D14

type D14 = D1 :* D4

#D13

type D13 = D1 :* D3

#D12

type D12 = D1 :* D2

#D11

type D11 = D1 :* D1

#D100

type D100 = (D1 :* D0) :* D0

#D10

type D10 = D1 :* D0

#d99

d99 :: D99

#d98

d98 :: D98

#d97

d97 :: D97

#d96

d96 :: D96

#d95

d95 :: D95

#d94

d94 :: D94

#d93

d93 :: D93

#d92

d92 :: D92

#d91

d91 :: D91

#d90

d90 :: D90

#d89

d89 :: D89

#d88

d88 :: D88

#d87

d87 :: D87

#d86

d86 :: D86

#d85

d85 :: D85

#d84

d84 :: D84

#d83

d83 :: D83

#d82

d82 :: D82

#d81

d81 :: D81

#d80

d80 :: D80

#d79

d79 :: D79

#d78

d78 :: D78

#d77

d77 :: D77

#d76

d76 :: D76

#d75

d75 :: D75

#d74

d74 :: D74

#d73

d73 :: D73

#d72

d72 :: D72

#d71

d71 :: D71

#d70

d70 :: D70

#d69

d69 :: D69

#d68

d68 :: D68

#d67

d67 :: D67

#d66

d66 :: D66

#d65

d65 :: D65

#d64

d64 :: D64

#d63

d63 :: D63

#d62

d62 :: D62

#d61

d61 :: D61

#d60

d60 :: D60

#d59

d59 :: D59

#d58

d58 :: D58

#d57

d57 :: D57

#d56

d56 :: D56

#d55

d55 :: D55

#d54

d54 :: D54

#d53

d53 :: D53

#d52

d52 :: D52

#d51

d51 :: D51

#d50

d50 :: D50

#d49

d49 :: D49

#d48

d48 :: D48

#d47

d47 :: D47

#d46

d46 :: D46

#d45

d45 :: D45

#d44

d44 :: D44

#d43

d43 :: D43

#d42

d42 :: D42

#d41

d41 :: D41

#d40

d40 :: D40

#d39

d39 :: D39

#d38

d38 :: D38

#d37

d37 :: D37

#d36

d36 :: D36

#d35

d35 :: D35

#d34

d34 :: D34

#d33

d33 :: D33

#d32

d32 :: D32

#d31

d31 :: D31

#d30

d30 :: D30

#d29

d29 :: D29

#d28

d28 :: D28

#d27

d27 :: D27

#d26

d26 :: D26

#d25

d25 :: D25

#d24

d24 :: D24

#d23

d23 :: D23

#d22

d22 :: D22

#d21

d21 :: D21

#d20

d20 :: D20

#d19

d19 :: D19

#d18

d18 :: D18

#d17

d17 :: D17

#d16

d16 :: D16

#d15

d15 :: D15

#d14

d14 :: D14

#d13

d13 :: D13

#d12

d12 :: D12

#d11

d11 :: D11

#d10

d10 :: D10

Re-exports from Data.Typelevel.Num.Ops

#PredecessorOfZeroError

data PredecessorOfZeroError :: forall k. k -> Typedata PredecessorOfZeroError t

#LT

data LT

Instances

(Nat x, Pos y) => DivModP x y D0 x LT
Show LT
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
(Pos (NumCons yi yl)) => Trich D0 (NumCons yi yl) LT
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
(Pos (NumCons yi yl)) => Trich D1 (NumCons yi yl) LT
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
(Pos (NumCons yi yl)) => Trich D2 (NumCons yi yl) LT
Trich D3 D4 LT
Trich D3 D5 LT
Trich D3 D6 LT
Trich D3 D7 LT
Trich D3 D8 LT
Trich D3 D9 LT
(Pos (NumCons yi yl)) => Trich D3 (NumCons yi yl) LT
Trich D4 D5 LT
Trich D4 D6 LT
Trich D4 D7 LT
Trich D4 D8 LT
Trich D4 D9 LT
(Pos (NumCons yi yl)) => Trich D4 (NumCons yi yl) LT
Trich D5 D6 LT
Trich D5 D7 LT
Trich D5 D8 LT
Trich D5 D9 LT
(Pos (NumCons yi yl)) => Trich D5 (NumCons yi yl) LT
Trich D6 D7 LT
Trich D6 D8 LT
Trich D6 D9 LT
(Pos (NumCons yi yl)) => Trich D6 (NumCons yi yl) LT
Trich D7 D8 LT
Trich D7 D9 LT
(Pos (NumCons yi yl)) => Trich D7 (NumCons yi yl) LT
Trich D8 D9 LT
(Pos (NumCons yi yl)) => Trich D8 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich D9 (NumCons yi yl) LT
CS LT r LT
MaxP x y LT y
(Nat x, Nat y, GCD y x gcd) => GCDP x y False LT gcd

#GT

data GT

Instances

(Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivModP x y q r GT
Show GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D0 GT
Trich D1 D0 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D1 GT
Trich D2 D0 GT
Trich D2 D1 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D2 GT
Trich D3 D0 GT
Trich D3 D1 GT
Trich D3 D2 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D3 GT
Trich D4 D0 GT
Trich D4 D1 GT
Trich D4 D2 GT
Trich D4 D3 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D4 GT
Trich D5 D0 GT
Trich D5 D1 GT
Trich D5 D2 GT
Trich D5 D3 GT
Trich D5 D4 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D5 GT
Trich D6 D0 GT
Trich D6 D1 GT
Trich D6 D2 GT
Trich D6 D3 GT
Trich D6 D4 GT
Trich D6 D5 GT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D6 GT
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
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D7 GT
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
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D8 GT
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
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D9 GT
CS GT r GT
MaxP x y GT x
(Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCDP x y False GT gcd

#EQ

data EQ

Instances

(Nat x, Pos y) => DivModP x y D1 D0 EQ
Show EQ
Trich D0 D0 EQ
Trich D1 D1 EQ
Trich D2 D2 EQ
Trich D3 D3 EQ
Trich D4 D4 EQ
Trich D5 D5 EQ
Trich D6 D6 EQ
Trich D7 D7 EQ
Trich D8 D8 EQ
Trich D9 D9 EQ
CS EQ r r
MaxP x y EQ y
(Nat x) => GCDP x x False EQ x

#Add

class Add :: forall k. Type -> Type -> k -> Constraintclass (AddP x y z, AddP y x z) <= Add x y z | x y -> z, z x -> y, z y -> x

Instances

(AddP x y z, AddP y x z) => Add x y z

#AddP

class AddP :: forall k1 k2. Type -> k1 -> k2 -> Constraintclass (Nat x) <= AddP x y z | x y -> z, z x -> y

Instances

(Nat y) => AddP D0 y y
(Succ y z) => AddP D1 y z
(Succ z z', AddP D1 y z) => AddP D2 y z'
(Succ z z', AddP D2 y z) => AddP D3 y z'
(Succ z z', AddP D3 y z) => AddP D4 y z'
(Succ z z', AddP D4 y z) => AddP D5 y z'
(Succ z z', AddP D5 y z) => AddP D6 y z'
(Succ z z', AddP D6 y z) => AddP D7 y z'
(Succ z z', AddP D7 y z) => AddP D8 y z'
(Succ z z', AddP D8 y z) => AddP D9 y z'
(Pos (NumCons xi xl), Nat z, AddP xi yi zi, DivMod10 y yi yl, AddP xl (NumCons zi yl) z) => AddP (NumCons xi xl) y z

#CS

class CS :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass CS r1 r2 r3 | r1 r2 -> r3

Instances

CS EQ r r
CS GT r GT
CS LT r LT

#Div

class Div :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Div x y z | x y -> z, x z -> y, y z -> x

Instances

(DivMod x y q r) => Div x y q

#Div10

class Div10 :: forall k. Type -> k -> Constraintclass (Nat x) <= Div10 x q | x -> q, q -> x

Instances

(DivMod10 x q r) => Div10 x q

#DivMod

class DivMod :: forall k1 k2. Type -> Type -> k1 -> k2 -> Constraintclass (Nat x, Pos y) <= DivMod x y q r | x y -> q r

Instances

(Nat x, Pos y, Trich x y cmp, DivModP x y q r cmp) => DivMod x y q r

#DivMod10

class DivMod10 :: forall k. Type -> Type -> k -> Constraintclass (Nat i, Nat x) <= DivMod10 x i l | i l -> x, x -> i l

Instances

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 (NumCons D1 l)) => DivMod10 (NumCons D1 l) D1 l
(Nat (NumCons D2 l)) => DivMod10 (NumCons D2 l) D2 l
(Nat (NumCons D3 l)) => DivMod10 (NumCons D3 l) D3 l
(Nat (NumCons D4 l)) => DivMod10 (NumCons D4 l) D4 l
(Nat (NumCons D5 l)) => DivMod10 (NumCons D5 l) D5 l
(Nat (NumCons D6 l)) => DivMod10 (NumCons D6 l) D6 l
(Nat (NumCons D7 l)) => DivMod10 (NumCons D7 l) D7 l
(Nat (NumCons D8 l)) => DivMod10 (NumCons D8 l) D8 l
(Nat (NumCons D9 l)) => DivMod10 (NumCons D9 l) D9 l
(Nat (NumCons x l), Nat (NumCons (NumCons x l) l')) => DivMod10 (NumCons (NumCons x l) l') (NumCons x l) l'

#DivModP

class DivModP :: forall k1 k2 k3. Type -> Type -> k1 -> k2 -> k3 -> Constraintclass (Nat x, Pos y) <= DivModP x y q r cmp | x y cmp -> q r, q r cmp y -> x, q r cmp x -> y

Instances

(Nat x, Pos y) => DivModP x y D0 x LT
(Nat x, Pos y) => DivModP x y D1 D0 EQ
(Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivModP x y q r GT

#Eq

class Eq :: forall k1 k2. k1 -> k2 -> Constraintclass Eq x y

Instances

(Trich x y EQ) => Eq x y

#Failure

class Failure :: forall k. k -> Constraintclass Failure t

#GCD

class (Nat x, Nat y, Nat gcd) <= GCD x y gcd | x y -> gcd

Instances

(Nat x, Nat y, Trich x y cmp, IsZero y yz, GCDP x y yz cmp gcd) => GCD x y gcd

#GCDP

class GCDP :: forall k1 k2. Type -> Type -> k1 -> k2 -> Type -> Constraintclass (Nat x, Nat y, Nat gcd) <= GCDP x y yz cmp gcd | x y yz cmp -> gcd

Instances

(Nat x) => GCDP x D0 True cmp D0
(Nat x, Nat y, GCD y x gcd) => GCDP x y False LT gcd
(Nat x) => GCDP x x False EQ x
(Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCDP x y False GT gcd

#Gt

class Gt :: forall k1 k2. k1 -> k2 -> Constraintclass Gt x y

Instances

(Trich x y GT) => Gt x y

#GtEq

class GtEq :: forall k1 k2. k1 -> k2 -> Constraintclass GtEq x y

Instances

(Succ x x', Trich x' y GT) => GtEq x y

#IsDivBy

class IsDivBy :: forall k. Type -> k -> Constraintclass (Pos d) <= IsDivBy d x

Instances

(DivMod x d q D0) => IsDivBy d x

#IsZero

class IsZero :: forall k1 k2. k1 -> k2 -> Constraintclass IsZero x r | x -> r

Instances

#Lt

class Lt :: forall k1 k2. k1 -> k2 -> Constraintclass Lt x y

Instances

(Trich x y LT) => Lt x y

#LtEq

class LtEq :: forall k1 k2. k1 -> k2 -> Constraintclass LtEq x y

Instances

(Succ y y', Trich x y' LT) => LtEq x y

#Max

class Max :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Max x y z | x y -> z

Instances

(MaxP x y b z, Trich x y b) => Max x y z

#MaxP

class MaxP :: forall k1 k2 k3 k4. k1 -> k2 -> k3 -> k4 -> Constraintclass MaxP x y b r | x y b -> r

Instances

MaxP x y LT y
MaxP x y EQ y
MaxP x y GT x

#Min

class Min :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Min x y z | x y -> z

Instances

(MaxP y x b z, Trich x y b) => Min x y z

#Mod

class Mod :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Mod x y r | x y -> r

Instances

(DivMod x y q r) => Mod x y r

#Mul

class Mul :: forall k. Type -> Type -> k -> Constraintclass (Nat x, Nat y) <= Mul x y z | x y -> z

Instances

(Nat y) => Mul D0 y D0
(Nat y) => Mul D1 y y
(Add y y z) => Mul D2 y z
(Add z y z', Mul D2 y z) => Mul D3 y z'
(Add z y z', Mul D3 y z) => Mul D4 y z'
(Add z y z', Mul D4 y z) => Mul D5 y z'
(Add z y z', Mul D5 y z) => Mul D6 y z'
(Add z y z', Mul D6 y z) => Mul D7 y z'
(Add z y z', Mul D7 y z) => Mul D8 y z'
(Add z y z', Mul D8 y z) => Mul D9 y z'
(Pos (NumCons xi xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, Add dy z10 z') => Mul (NumCons xi xl) y z'

#Mul10

class Mul10 :: forall k. k -> Type -> Constraintclass (Nat q) <= Mul10 x q | x -> q, q -> x

Instances

(DivMod10 x q D0) => Mul10 q x

#Pred

class Pred :: forall k. Type -> k -> Constraintclass (Pos x) <= Pred x y | x -> y, y -> x

Instances

(Succ x y) => Pred y x

#Sub

class Sub :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Sub x y z | x y -> z, z x -> y, z y -> x

Instances

(Add x y z) => Sub z y x

#Succ

class (Nat x, Pos y) <= Succ x y | x -> y, y -> x

Instances

(Pos y, IsZero y yz, DivMod10 x xi xl, SuccP xi xl yi yl yz, DivMod10 y yi yl) => Succ x y

#SuccP

class SuccP :: forall k1 k2 k3 k4 k5. k1 -> k2 -> k3 -> k4 -> k5 -> Constraintclass SuccP xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xl

Instances

(Failure (PredecessorOfZeroError x)) => SuccP (Tuple x x) (Tuple x x) D0 D0 True
SuccP xi D0 xi D1 False
SuccP xi D1 xi D2 False
SuccP xi D2 xi D3 False
SuccP xi D3 xi D4 False
SuccP xi D4 xi D5 False
SuccP xi D5 xi D6 False
SuccP xi D6 xi D7 False
SuccP xi D7 xi D8 False
SuccP xi D8 xi D9 False
(Succ xi yi) => SuccP xi D9 yi D0 False

#Trich

class Trich :: forall k. Type -> Type -> k -> Constraintclass (Nat x, Nat y) <= Trich x y r | x y -> r

Instances

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
(Pos (NumCons yi yl)) => Trich D0 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D0 GT
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
(Pos (NumCons yi yl)) => Trich D1 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D1 GT
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
(Pos (NumCons yi yl)) => Trich D2 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D2 GT
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
(Pos (NumCons yi yl)) => Trich D3 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D3 GT
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
(Pos (NumCons yi yl)) => Trich D4 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D4 GT
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
(Pos (NumCons yi yl)) => Trich D5 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D5 GT
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
(Pos (NumCons yi yl)) => Trich D6 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D6 GT
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
(Pos (NumCons yi yl)) => Trich D7 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D7 GT
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
(Pos (NumCons yi yl)) => Trich D8 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D8 GT
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
(Pos (NumCons yi yl)) => Trich D9 (NumCons yi yl) LT
(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D9 GT
(Pos (NumCons xi xl), Pos (NumCons yi yl), Trich xl yl rl, Trich xi yi ri, CS ri rl r) => Trich (NumCons xi xl) (NumCons yi yl) r

#trich

trich :: forall x y r. Trich x y r => x -> y -> r

#succ

succ :: forall x y. Succ x y => x -> y

#sub

sub :: forall x y z. Sub x y z => x -> y -> z

#pred

pred :: forall x y. Pred x y => x -> y

#mul10

mul10 :: forall x q. Mul10 x q => x -> q

#mul

mul :: forall x y z. Mul x y z => x -> y -> z

#mod

mod :: forall x y r. Mod x y r => x -> y -> r

#min

min :: forall x y z. Min x y z => x -> y -> z

#max

max :: forall x y z. Max x y z => x -> y -> z

#lteq

lteq :: forall x y. LtEq x y => x -> y -> Unit

#lt

lt :: forall x y. Lt x y => x -> y -> Unit

#isDivBy

isDivBy :: forall d x. IsDivBy d x => d -> x

#gteq

gteq :: forall x y. GtEq x y => x -> y -> Unit

#gt

gt :: forall x y. Gt x y => x -> y -> Unit

#gcd

gcd :: forall x y z. GCD x y z => x -> y -> z

#eq

eq :: forall x y. Eq x y => x -> y -> Unit

#divMod10

divMod10 :: forall x r q. DivMod10 x q r => x -> Tuple q r

#divMod

divMod :: forall x y q r. DivMod x y q r => x -> y -> Tuple q r

#div10

div10 :: forall x q. Div10 x q => x -> q

#div

div :: forall x y z. Div x y z => x -> y -> z

#add

add :: forall x y z. Add x y z => x -> y -> z

#(>=)

Operator alias for Data.Typelevel.Num.Ops.gteq (left-associative / precedence 4)

#(>)

Operator alias for Data.Typelevel.Num.Ops.gt (left-associative / precedence 4)

#(==)

Operator alias for Data.Typelevel.Num.Ops.eq (left-associative / precedence 4)

#(<=)

Operator alias for Data.Typelevel.Num.Ops.lteq (left-associative / precedence 4)

#(<)

Operator alias for Data.Typelevel.Num.Ops.lt (left-associative / precedence 4)

#(-)

Operator alias for Data.Typelevel.Num.Ops.sub (left-associative / precedence 6)

#(+)

Operator alias for Data.Typelevel.Num.Ops.add (left-associative / precedence 6)

#(*)

Operator alias for Data.Typelevel.Num.Ops.mul (left-associative / precedence 7)

Re-exports from Data.Typelevel.Num.Reps

#NumCons

data NumCons a b

Constructors

NumCons a b

Instances

(Show a, Show b) => Show (NumCons a b)

#D9

data D9

Instances

Show D9

#D8

data D8

Instances

Show D8

#D7

data D7

Instances

Show D7

#D6

data D6

Instances

Show D6

#D5

data D5

Instances

Show D5

#D4

data D4

Instances

Show D4

#D3

data D3

Instances

Show D3

#D2

data D2

Instances

Show D2

#D1

data D1

Instances

Show D1

#D0

data D0

Instances

Show D0

#d9

d9 :: D9

#d8

d8 :: D8

#d7

d7 :: D7

#d6

d6 :: D6

#d5

d5 :: D5

#d4

d4 :: D4

#d3

d3 :: D3

#d2

d2 :: D2

#d1

d1 :: D1

#d0

d0 :: D0

#type (:*)

Operator alias for Data.Typelevel.Num.Reps.NumCons (non-associative / precedence 6)

Re-exports from Data.Typelevel.Num.Sets

#Nat

class Nat n  where

Members

toInt :: n -> Int

Instances

Nat D0
Nat D1
Nat D2
Nat D3
Nat D4
Nat D5
Nat D6
Nat D7
Nat D8
Nat D9
(Pos x) => Nat (NumCons x D0)
(Pos x) => Nat (NumCons x D1)
(Pos x) => Nat (NumCons x D2)
(Pos x) => Nat (NumCons x D3)
(Pos x) => Nat (NumCons x D4)
(Pos x) => Nat (NumCons x D5)
(Pos x) => Nat (NumCons x D6)
(Pos x) => Nat (NumCons x D7)
(Pos x) => Nat (NumCons x D8)
(Pos x) => Nat (NumCons x D9)

#Pos

class (Nat n) <= Pos n

Instances

Pos D1
Pos D2
Pos D3
Pos D4
Pos D5
Pos D6
Pos D7
Pos D8
Pos D9
(Pos x) => Pos (NumCons x D0)
(Pos x) => Pos (NumCons x D1)
(Pos x) => Pos (NumCons x D2)
(Pos x) => Pos (NumCons x D3)
(Pos x) => Pos (NumCons x D4)
(Pos x) => Pos (NumCons x D5)
(Pos x) => Pos (NumCons x D6)
(Pos x) => Pos (NumCons x D7)
(Pos x) => Pos (NumCons x D8)
(Pos x) => Pos (NumCons x D9)

#toInt'

toInt' :: forall n. Nat n => Proxy n -> Int

Sugar for toInt, providing a more intuitive type

#subLastDec

subLastDec :: forall x d. Nat (x :* d) => Nat x => x :* d -> Int

#reifyIntP

reifyIntP :: forall r. Int -> (forall n. Pos n => n -> r) -> r

#reifyInt

reifyInt :: forall r. Int -> (forall n. Nat n => n -> r) -> r

#div10Dec

div10Dec :: forall x d. Nat (x :* d) => x :* d -> x