Module

Type.Data.Peano.Nat

Re-exports from Type.Data.Peano.Nat.Definition

#Z

data Z :: Nat

Represents 0

Instances

IsNat Z
SumNat a Z a
SumNat Z a a
ProductNat Z a Z
0 * a = 0
ProductNat (Succ Z) a a
1 * a = a
ExponentiationNat a Z (Succ Z)
CompareNat Z a LT
CompareNat a Z GT
IsZeroNat Z True

#Succ

data Succ :: Nat -> Nat

Represents Successor of a Nat: (Succ a) ^= 1 + a

Instances

(IsNat a) => IsNat (Succ a)
(SumNat a b c) => SumNat (Succ a) b (Succ c)
ProductNat (Succ Z) a a
1 * a = a
(ProductNat a b ab, SumNat ab b result) => ProductNat (Succ a) b result
ExponentiationNat a Z (Succ Z)
(ExponentiationNat a b ab, ProductNat ab a result) => ExponentiationNat a (Succ b) result
(CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
IsZeroNat (Succ a) False
Pred (Succ a) a

#Nat

data Nat

Represents a non-negative whole Number ℕ₀

#NProxy

data NProxy (n :: Nat)

Constructors

NProxy

Instances

(IsNat a) => Show (NProxy a)

#CompareNat

class CompareNat (a :: Nat) (b :: Nat) (ord :: Ordering) | a b -> ord

Instances

CompareNat a a EQ
CompareNat Z a LT
CompareNat a Z GT
(CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord

#ExponentiationNat

class ExponentiationNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

Instances

ExponentiationNat a Z (Succ Z)
(ExponentiationNat a b ab, ProductNat ab a result) => ExponentiationNat a (Succ b) result

#IsNat

class IsNat (a :: Nat)  where

Members

reflectNat :: forall proxy. proxy a -> Int
reflect typelevel Nat to a valuelevel Int
```
reflectNat (Proxy  :: _ D10) = 10
reflectNat (NProxy :: _ D10) = 10
```

Instances

IsNat Z
(IsNat a) => IsNat (Succ a)

#IsZeroNat

class IsZeroNat (a :: Nat) (isZero :: Boolean) | a -> isZero

Instances

IsZeroNat Z True
IsZeroNat (Succ a) False

#ProductNat

class ProductNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

a * b = c

Instances

ProductNat Z a Z
0 * a = 0
ProductNat (Succ Z) a a
1 * a = a
(ProductNat a b ab, SumNat ab b result) => ProductNat (Succ a) b result

#SumNat

class SumNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

a + b = c

Instances

SumNat a Z a
SumNat Z a a
(SumNat a b c) => SumNat (Succ a) b (Succ c)

#showNat

showNat :: forall proxy n. IsNat n => proxy n -> String

#powNat

powNat :: forall proxy a b c. ExponentiationNat a b c => proxy a -> proxy b -> proxy c

> powNat d2 d3
8 -- : NProxy D8

a raised to the power of b a^b = c

#plusNat

plusNat :: forall proxy a b c. SumNat a b c => proxy a -> proxy b -> proxy c

#mulNat

mulNat :: forall proxy a b c. ProductNat a b c => proxy a -> proxy b -> proxy c

Re-exports from Type.Data.Peano.Nat.Parse

#ParseNat

class ParseNat (sym :: Symbol) (nat :: Nat) | nat -> sym, sym -> nat

Parses a Nat from a Symbol

ParseNat "2" ~> (Succ (Succ Z))
ParseNat "1283" ~> (Succ (...))

Instances

ParseNat "0" Z
ParseNat "1" (Succ Z)
ParseNat "2" (Succ (Succ Z))
ParseNat "3" (Succ (Succ (Succ Z)))
ParseNat "4" (Succ (Succ (Succ (Succ Z))))
ParseNat "5" (Succ (Succ (Succ (Succ (Succ Z)))))
ParseNat "6" (Succ (Succ (Succ (Succ (Succ (Succ Z))))))
ParseNat "7" (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))
ParseNat "8" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))
ParseNat "9" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))))
(ParseNat head msd, Cons head tail sym, Length tail symLength, ExponentiationNat D10 symLength offset, ProductNat offset msd high, ParseNat tail lower, SumNat high lower res) => ParseNat sym res

#parseNat

parseNat :: forall sproxy proxy sym a. ParseNat sym a => sproxy sym -> proxy a

value-level parse of number

parseNat (Proxy  "10") ~> D10
parseNat (SProxy "10") ~> D10

Re-exports from Type.Data.Peano.Nat.TypeAliases

#D99

type D99 = Succ D98

#D98

type D98 = Succ D97

#D97

type D97 = Succ D96

#D96

type D96 = Succ D95

#D95

type D95 = Succ D94

#D94

type D94 = Succ D93

#D93

type D93 = Succ D92

#D92

type D92 = Succ D91

#D91

type D91 = Succ D90

#D90

type D90 = Succ D89

#D9

type D9 = Succ D8

#D89

type D89 = Succ D88

#D88

type D88 = Succ D87

#D87

type D87 = Succ D86

#D86

type D86 = Succ D85

#D85

type D85 = Succ D84

#D84

type D84 = Succ D83

#D83

type D83 = Succ D82

#D82

type D82 = Succ D81

#D81

type D81 = Succ D80

#D80

type D80 = Succ D79

#D8

type D8 = Succ D7

#D79

type D79 = Succ D78

#D78

type D78 = Succ D77

#D77

type D77 = Succ D76

#D76

type D76 = Succ D75

#D75

type D75 = Succ D74

#D74

type D74 = Succ D73

#D73

type D73 = Succ D72

#D72

type D72 = Succ D71

#D71

type D71 = Succ D70

#D70

type D70 = Succ D69

#D7

type D7 = Succ D6

#D69

type D69 = Succ D68

#D68

type D68 = Succ D67

#D67

type D67 = Succ D66

#D66

type D66 = Succ D65

#D65

type D65 = Succ D64

#D64

type D64 = Succ D63

#D63

type D63 = Succ D62

#D62

type D62 = Succ D61

#D61

type D61 = Succ D60

#D60

type D60 = Succ D59

#D6

type D6 = Succ D5

#D59

type D59 = Succ D58

#D58

type D58 = Succ D57

#D57

type D57 = Succ D56

#D56

type D56 = Succ D55

#D55

type D55 = Succ D54

#D54

type D54 = Succ D53

#D53

type D53 = Succ D52

#D52

type D52 = Succ D51

#D51

type D51 = Succ D50

#D50

type D50 = Succ D49

#D5

type D5 = Succ D4

#D49

type D49 = Succ D48

#D48

type D48 = Succ D47

#D47

type D47 = Succ D46

#D46

type D46 = Succ D45

#D45

type D45 = Succ D44

#D44

type D44 = Succ D43

#D43

type D43 = Succ D42

#D42

type D42 = Succ D41

#D41

type D41 = Succ D40

#D40

type D40 = Succ D39

#D4

type D4 = Succ D3

#D39

type D39 = Succ D38

#D38

type D38 = Succ D37

#D37

type D37 = Succ D36

#D36

type D36 = Succ D35

#D35

type D35 = Succ D34

#D34

type D34 = Succ D33

#D33

type D33 = Succ D32

#D32

type D32 = Succ D31

#D31

type D31 = Succ D30

#D30

type D30 = Succ D29

#D3

type D3 = Succ D2

#D29

type D29 = Succ D28

#D28

type D28 = Succ D27

#D27

type D27 = Succ D26

#D26

type D26 = Succ D25

#D25

type D25 = Succ D24

#D24

type D24 = Succ D23

#D23

type D23 = Succ D22

#D22

type D22 = Succ D21

#D21

type D21 = Succ D20

#D20

type D20 = Succ D19

#D2

type D2 = Succ D1

#D19

type D19 = Succ D18

#D18

type D18 = Succ D17

#D17

type D17 = Succ D16

#D16

type D16 = Succ D15

#D15

type D15 = Succ D14

#D14

type D14 = Succ D13

#D13

type D13 = Succ D12

#D12

type D12 = Succ D11

#D11

type D11 = Succ D10

#D100

type D100 = Succ D99

#D10

type D10 = Succ D9

#D1

type D1 = Succ D0

#D0

type D0 = Z

#d99

d99 :: forall proxy. proxy D99

#d98

d98 :: forall proxy. proxy D98

#d97

d97 :: forall proxy. proxy D97

#d96

d96 :: forall proxy. proxy D96

#d95

d95 :: forall proxy. proxy D95

#d94

d94 :: forall proxy. proxy D94

#d93

d93 :: forall proxy. proxy D93

#d92

d92 :: forall proxy. proxy D92

#d91

d91 :: forall proxy. proxy D91

#d90

d90 :: forall proxy. proxy D90

#d9

d9 :: forall proxy. proxy D9

#d89

d89 :: forall proxy. proxy D89

#d88

d88 :: forall proxy. proxy D88

#d87

d87 :: forall proxy. proxy D87

#d86

d86 :: forall proxy. proxy D86

#d85

d85 :: forall proxy. proxy D85

#d84

d84 :: forall proxy. proxy D84

#d83

d83 :: forall proxy. proxy D83

#d82

d82 :: forall proxy. proxy D82

#d81

d81 :: forall proxy. proxy D81

#d80

d80 :: forall proxy. proxy D80

#d8

d8 :: forall proxy. proxy D8

#d79

d79 :: forall proxy. proxy D79

#d78

d78 :: forall proxy. proxy D78

#d77

d77 :: forall proxy. proxy D77

#d76

d76 :: forall proxy. proxy D76

#d75

d75 :: forall proxy. proxy D75

#d74

d74 :: forall proxy. proxy D74

#d73

d73 :: forall proxy. proxy D73

#d72

d72 :: forall proxy. proxy D72

#d71

d71 :: forall proxy. proxy D71

#d70

d70 :: forall proxy. proxy D70

#d7

d7 :: forall proxy. proxy D7

#d69

d69 :: forall proxy. proxy D69

#d68

d68 :: forall proxy. proxy D68

#d67

d67 :: forall proxy. proxy D67

#d66

d66 :: forall proxy. proxy D66

#d65

d65 :: forall proxy. proxy D65

#d64

d64 :: forall proxy. proxy D64

#d63

d63 :: forall proxy. proxy D63

#d62

d62 :: forall proxy. proxy D62

#d61

d61 :: forall proxy. proxy D61

#d60

d60 :: forall proxy. proxy D60

#d6

d6 :: forall proxy. proxy D6

#d59

d59 :: forall proxy. proxy D59

#d58

d58 :: forall proxy. proxy D58

#d57

d57 :: forall proxy. proxy D57

#d56

d56 :: forall proxy. proxy D56

#d55

d55 :: forall proxy. proxy D55

#d54

d54 :: forall proxy. proxy D54

#d53

d53 :: forall proxy. proxy D53

#d52

d52 :: forall proxy. proxy D52

#d51

d51 :: forall proxy. proxy D51

#d50

d50 :: forall proxy. proxy D50

#d5

d5 :: forall proxy. proxy D5

#d49

d49 :: forall proxy. proxy D49

#d48

d48 :: forall proxy. proxy D48

#d47

d47 :: forall proxy. proxy D47

#d46

d46 :: forall proxy. proxy D46

#d45

d45 :: forall proxy. proxy D45

#d44

d44 :: forall proxy. proxy D44

#d43

d43 :: forall proxy. proxy D43

#d42

d42 :: forall proxy. proxy D42

#d41

d41 :: forall proxy. proxy D41

#d40

d40 :: forall proxy. proxy D40

#d4

d4 :: forall proxy. proxy D4

#d39

d39 :: forall proxy. proxy D39

#d38

d38 :: forall proxy. proxy D38

#d37

d37 :: forall proxy. proxy D37

#d36

d36 :: forall proxy. proxy D36

#d35

d35 :: forall proxy. proxy D35

#d34

d34 :: forall proxy. proxy D34

#d33

d33 :: forall proxy. proxy D33

#d32

d32 :: forall proxy. proxy D32

#d31

d31 :: forall proxy. proxy D31

#d30

d30 :: forall proxy. proxy D30

#d3

d3 :: forall proxy. proxy D3

#d29

d29 :: forall proxy. proxy D29

#d28

d28 :: forall proxy. proxy D28

#d27

d27 :: forall proxy. proxy D27

#d26

d26 :: forall proxy. proxy D26

#d25

d25 :: forall proxy. proxy D25

#d24

d24 :: forall proxy. proxy D24

#d23

d23 :: forall proxy. proxy D23

#d22

d22 :: forall proxy. proxy D22

#d21

d21 :: forall proxy. proxy D21

#d20

d20 :: forall proxy. proxy D20

#d2

d2 :: forall proxy. proxy D2

#d19

d19 :: forall proxy. proxy D19

#d18

d18 :: forall proxy. proxy D18

#d17

d17 :: forall proxy. proxy D17

#d16

d16 :: forall proxy. proxy D16

#d15

d15 :: forall proxy. proxy D15

#d14

d14 :: forall proxy. proxy D14

#d13

d13 :: forall proxy. proxy D13

#d12

d12 :: forall proxy. proxy D12

#d11

d11 :: forall proxy. proxy D11

#d100

d100 :: forall proxy. proxy D100

#d10

d10 :: forall proxy. proxy D10

#d1

d1 :: forall proxy. proxy D1

#d0

d0 :: forall proxy. proxy D0