Module

Type.Data.Peano.Nat

Package: purescript-typelevel-peano
Repository: csicar/purescript-typelevel-peano

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

#Z Source

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 Source

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 Source

data Nat

Represents a non-negative whole Number ℕ₀

#NProxy Source

data NProxy (n :: Nat)

Constructors

NProxy

Instances

(IsNat a) => Show (NProxy a)

#CompareNat Source

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 Source

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 Source

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 Source

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

Instances

IsZeroNat Z True
IsZeroNat (Succ a) False

#ProductNat Source

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 Source

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 Source

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

#powNat Source

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 Source

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

#mulNat Source

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 Source

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 Source

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 Source

type D99 = Succ D98

#D98 Source

type D98 = Succ D97

#D97 Source

type D97 = Succ D96

#D96 Source

type D96 = Succ D95

#D95 Source

type D95 = Succ D94

#D94 Source

type D94 = Succ D93

#D93 Source

type D93 = Succ D92

#D92 Source

type D92 = Succ D91

#D91 Source

type D91 = Succ D90

#D90 Source

type D90 = Succ D89

#D9 Source

type D9 = Succ D8

#D89 Source

type D89 = Succ D88

#D88 Source

type D88 = Succ D87

#D87 Source

type D87 = Succ D86

#D86 Source

type D86 = Succ D85

#D85 Source

type D85 = Succ D84

#D84 Source

type D84 = Succ D83

#D83 Source

type D83 = Succ D82

#D82 Source

type D82 = Succ D81

#D81 Source

type D81 = Succ D80

#D80 Source

type D80 = Succ D79

#D8 Source

type D8 = Succ D7

#D79 Source

type D79 = Succ D78

#D78 Source

type D78 = Succ D77

#D77 Source

type D77 = Succ D76

#D76 Source

type D76 = Succ D75

#D75 Source

type D75 = Succ D74

#D74 Source

type D74 = Succ D73

#D73 Source

type D73 = Succ D72

#D72 Source

type D72 = Succ D71

#D71 Source

type D71 = Succ D70

#D70 Source

type D70 = Succ D69

#D7 Source

type D7 = Succ D6

#D69 Source

type D69 = Succ D68

#D68 Source

type D68 = Succ D67

#D67 Source

type D67 = Succ D66

#D66 Source

type D66 = Succ D65

#D65 Source

type D65 = Succ D64

#D64 Source

type D64 = Succ D63

#D63 Source

type D63 = Succ D62

#D62 Source

type D62 = Succ D61

#D61 Source

type D61 = Succ D60

#D60 Source

type D60 = Succ D59

#D6 Source

type D6 = Succ D5

#D59 Source

type D59 = Succ D58

#D58 Source

type D58 = Succ D57

#D57 Source

type D57 = Succ D56

#D56 Source

type D56 = Succ D55

#D55 Source

type D55 = Succ D54

#D54 Source

type D54 = Succ D53

#D53 Source

type D53 = Succ D52

#D52 Source

type D52 = Succ D51

#D51 Source

type D51 = Succ D50

#D50 Source

type D50 = Succ D49

#D5 Source

type D5 = Succ D4

#D49 Source

type D49 = Succ D48

#D48 Source

type D48 = Succ D47

#D47 Source

type D47 = Succ D46

#D46 Source

type D46 = Succ D45

#D45 Source

type D45 = Succ D44

#D44 Source

type D44 = Succ D43

#D43 Source

type D43 = Succ D42

#D42 Source

type D42 = Succ D41

#D41 Source

type D41 = Succ D40

#D40 Source

type D40 = Succ D39

#D4 Source

type D4 = Succ D3

#D39 Source

type D39 = Succ D38

#D38 Source

type D38 = Succ D37

#D37 Source

type D37 = Succ D36

#D36 Source

type D36 = Succ D35

#D35 Source

type D35 = Succ D34

#D34 Source

type D34 = Succ D33

#D33 Source

type D33 = Succ D32

#D32 Source

type D32 = Succ D31

#D31 Source

type D31 = Succ D30

#D30 Source

type D30 = Succ D29

#D3 Source

type D3 = Succ D2

#D29 Source

type D29 = Succ D28

#D28 Source

type D28 = Succ D27

#D27 Source

type D27 = Succ D26

#D26 Source

type D26 = Succ D25

#D25 Source

type D25 = Succ D24

#D24 Source

type D24 = Succ D23

#D23 Source

type D23 = Succ D22

#D22 Source

type D22 = Succ D21

#D21 Source

type D21 = Succ D20

#D20 Source

type D20 = Succ D19

#D2 Source

type D2 = Succ D1

#D19 Source

type D19 = Succ D18

#D18 Source

type D18 = Succ D17

#D17 Source

type D17 = Succ D16

#D16 Source

type D16 = Succ D15

#D15 Source

type D15 = Succ D14

#D14 Source

type D14 = Succ D13

#D13 Source

type D13 = Succ D12

#D12 Source

type D12 = Succ D11

#D11 Source

type D11 = Succ D10

#D100 Source

type D100 = Succ D99

#D10 Source

type D10 = Succ D9

#D1 Source

type D1 = Succ D0

#D0 Source

type D0 = Z

#d99 Source

d99 :: forall proxy. proxy D99

#d98 Source

d98 :: forall proxy. proxy D98

#d97 Source

d97 :: forall proxy. proxy D97

#d96 Source

d96 :: forall proxy. proxy D96

#d95 Source

d95 :: forall proxy. proxy D95

#d94 Source

d94 :: forall proxy. proxy D94

#d93 Source

d93 :: forall proxy. proxy D93

#d92 Source

d92 :: forall proxy. proxy D92

#d91 Source

d91 :: forall proxy. proxy D91

#d90 Source

d90 :: forall proxy. proxy D90

#d9 Source

d9 :: forall proxy. proxy D9

#d89 Source

d89 :: forall proxy. proxy D89

#d88 Source

d88 :: forall proxy. proxy D88

#d87 Source

d87 :: forall proxy. proxy D87

#d86 Source

d86 :: forall proxy. proxy D86

#d85 Source

d85 :: forall proxy. proxy D85

#d84 Source

d84 :: forall proxy. proxy D84

#d83 Source

d83 :: forall proxy. proxy D83

#d82 Source

d82 :: forall proxy. proxy D82

#d81 Source

d81 :: forall proxy. proxy D81

#d80 Source

d80 :: forall proxy. proxy D80

#d8 Source

d8 :: forall proxy. proxy D8

#d79 Source

d79 :: forall proxy. proxy D79

#d78 Source

d78 :: forall proxy. proxy D78

#d77 Source

d77 :: forall proxy. proxy D77

#d76 Source

d76 :: forall proxy. proxy D76

#d75 Source

d75 :: forall proxy. proxy D75

#d74 Source

d74 :: forall proxy. proxy D74

#d73 Source

d73 :: forall proxy. proxy D73

#d72 Source

d72 :: forall proxy. proxy D72

#d71 Source

d71 :: forall proxy. proxy D71

#d70 Source

d70 :: forall proxy. proxy D70

#d7 Source

d7 :: forall proxy. proxy D7

#d69 Source

d69 :: forall proxy. proxy D69

#d68 Source

d68 :: forall proxy. proxy D68

#d67 Source

d67 :: forall proxy. proxy D67

#d66 Source

d66 :: forall proxy. proxy D66

#d65 Source

d65 :: forall proxy. proxy D65

#d64 Source

d64 :: forall proxy. proxy D64

#d63 Source

d63 :: forall proxy. proxy D63

#d62 Source

d62 :: forall proxy. proxy D62

#d61 Source

d61 :: forall proxy. proxy D61

#d60 Source

d60 :: forall proxy. proxy D60

#d6 Source

d6 :: forall proxy. proxy D6

#d59 Source

d59 :: forall proxy. proxy D59

#d58 Source

d58 :: forall proxy. proxy D58

#d57 Source

d57 :: forall proxy. proxy D57

#d56 Source

d56 :: forall proxy. proxy D56

#d55 Source

d55 :: forall proxy. proxy D55

#d54 Source

d54 :: forall proxy. proxy D54

#d53 Source

d53 :: forall proxy. proxy D53

#d52 Source

d52 :: forall proxy. proxy D52

#d51 Source

d51 :: forall proxy. proxy D51

#d50 Source

d50 :: forall proxy. proxy D50

#d5 Source

d5 :: forall proxy. proxy D5

#d49 Source

d49 :: forall proxy. proxy D49

#d48 Source

d48 :: forall proxy. proxy D48

#d47 Source

d47 :: forall proxy. proxy D47

#d46 Source

d46 :: forall proxy. proxy D46

#d45 Source

d45 :: forall proxy. proxy D45

#d44 Source

d44 :: forall proxy. proxy D44

#d43 Source

d43 :: forall proxy. proxy D43

#d42 Source

d42 :: forall proxy. proxy D42

#d41 Source

d41 :: forall proxy. proxy D41

#d40 Source

d40 :: forall proxy. proxy D40

#d4 Source

d4 :: forall proxy. proxy D4

#d39 Source

d39 :: forall proxy. proxy D39

#d38 Source

d38 :: forall proxy. proxy D38

#d37 Source

d37 :: forall proxy. proxy D37

#d36 Source

d36 :: forall proxy. proxy D36

#d35 Source

d35 :: forall proxy. proxy D35

#d34 Source

d34 :: forall proxy. proxy D34

#d33 Source

d33 :: forall proxy. proxy D33

#d32 Source

d32 :: forall proxy. proxy D32

#d31 Source

d31 :: forall proxy. proxy D31

#d30 Source

d30 :: forall proxy. proxy D30

#d3 Source

d3 :: forall proxy. proxy D3

#d29 Source

d29 :: forall proxy. proxy D29

#d28 Source

d28 :: forall proxy. proxy D28

#d27 Source

d27 :: forall proxy. proxy D27

#d26 Source

d26 :: forall proxy. proxy D26

#d25 Source

d25 :: forall proxy. proxy D25

#d24 Source

d24 :: forall proxy. proxy D24

#d23 Source

d23 :: forall proxy. proxy D23

#d22 Source

d22 :: forall proxy. proxy D22

#d21 Source

d21 :: forall proxy. proxy D21

#d20 Source

d20 :: forall proxy. proxy D20

#d2 Source

d2 :: forall proxy. proxy D2

#d19 Source

d19 :: forall proxy. proxy D19

#d18 Source

d18 :: forall proxy. proxy D18

#d17 Source

d17 :: forall proxy. proxy D17

#d16 Source

d16 :: forall proxy. proxy D16

#d15 Source

d15 :: forall proxy. proxy D15

#d14 Source

d14 :: forall proxy. proxy D14

#d13 Source

d13 :: forall proxy. proxy D13

#d12 Source

d12 :: forall proxy. proxy D12

#d11 Source

d11 :: forall proxy. proxy D11

#d100 Source

d100 :: forall proxy. proxy D100

#d10 Source

d10 :: forall proxy. proxy D10

#d1 Source

d1 :: forall proxy. proxy D1

#d0 Source

d0 :: forall proxy. proxy D0

Modules: Type.Data.Peano; Type.Data.Peano.Int; Type.Data.Peano.Int.Definition; Type.Data.Peano.Int.Parse; Type.Data.Peano.Int.TypeAliases; Type.Data.Peano.Nat; Type.Data.Peano.Nat.Definition; Type.Data.Peano.Nat.Parse; Type.Data.Peano.Nat.TypeAliases