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
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
(CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
IsZeroNat (Succ a) False

#NProxy Source

data NProxy (n :: Nat)

Proxy from kind Nat to kind Type

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

#IsNat Source

class IsNat (a :: Nat)  where

Members

reflectNat :: NProxy a -> Int
reflect typelevel Nat to a valuelevel Int
```
reflectNat (undefined :: 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)

#plusNat Source

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

#mulNat Source

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

#Nat Source

data Nat :: Type

Represents a non-negative whole Number ℕ₀

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, ProductNat msd D10 high, ParseNat tail lower, SumNat high lower res) => ParseNat sym res

#parseNat Source

parseNat :: forall sym a. ParseNat sym a => SProxy sym -> NProxy a

value-level parse of number

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 :: NProxy D99

#d98 Source

d98 :: NProxy D98

#d97 Source

d97 :: NProxy D97

#d96 Source

d96 :: NProxy D96

#d95 Source

d95 :: NProxy D95

#d94 Source

d94 :: NProxy D94

#d93 Source

d93 :: NProxy D93

#d92 Source

d92 :: NProxy D92

#d91 Source

d91 :: NProxy D91

#d90 Source

d90 :: NProxy D90

#d9 Source

d9 :: NProxy D9

#d89 Source

d89 :: NProxy D89

#d88 Source

d88 :: NProxy D88

#d87 Source

d87 :: NProxy D87

#d86 Source

d86 :: NProxy D86

#d85 Source

d85 :: NProxy D85

#d84 Source

d84 :: NProxy D84

#d83 Source

d83 :: NProxy D83

#d82 Source

d82 :: NProxy D82

#d81 Source

d81 :: NProxy D81

#d80 Source

d80 :: NProxy D80

#d8 Source

d8 :: NProxy D8

#d79 Source

d79 :: NProxy D79

#d78 Source

d78 :: NProxy D78

#d77 Source

d77 :: NProxy D77

#d76 Source

d76 :: NProxy D76

#d75 Source

d75 :: NProxy D75

#d74 Source

d74 :: NProxy D74

#d73 Source

d73 :: NProxy D73

#d72 Source

d72 :: NProxy D72

#d71 Source

d71 :: NProxy D71

#d70 Source

d70 :: NProxy D70

#d7 Source

d7 :: NProxy D7

#d69 Source

d69 :: NProxy D69

#d68 Source

d68 :: NProxy D68

#d67 Source

d67 :: NProxy D67

#d66 Source

d66 :: NProxy D66

#d65 Source

d65 :: NProxy D65

#d64 Source

d64 :: NProxy D64

#d63 Source

d63 :: NProxy D63

#d62 Source

d62 :: NProxy D62

#d61 Source

d61 :: NProxy D61

#d60 Source

d60 :: NProxy D60

#d6 Source

d6 :: NProxy D6

#d59 Source

d59 :: NProxy D59

#d58 Source

d58 :: NProxy D58

#d57 Source

d57 :: NProxy D57

#d56 Source

d56 :: NProxy D56

#d55 Source

d55 :: NProxy D55

#d54 Source

d54 :: NProxy D54

#d53 Source

d53 :: NProxy D53

#d52 Source

d52 :: NProxy D52

#d51 Source

d51 :: NProxy D51

#d50 Source

d50 :: NProxy D50

#d5 Source

d5 :: NProxy D5

#d49 Source

d49 :: NProxy D49

#d48 Source

d48 :: NProxy D48

#d47 Source

d47 :: NProxy D47

#d46 Source

d46 :: NProxy D46

#d45 Source

d45 :: NProxy D45

#d44 Source

d44 :: NProxy D44

#d43 Source

d43 :: NProxy D43

#d42 Source

d42 :: NProxy D42

#d41 Source

d41 :: NProxy D41

#d40 Source

d40 :: NProxy D40

#d4 Source

d4 :: NProxy D4

#d39 Source

d39 :: NProxy D39

#d38 Source

d38 :: NProxy D38

#d37 Source

d37 :: NProxy D37

#d36 Source

d36 :: NProxy D36

#d35 Source

d35 :: NProxy D35

#d34 Source

d34 :: NProxy D34

#d33 Source

d33 :: NProxy D33

#d32 Source

d32 :: NProxy D32

#d31 Source

d31 :: NProxy D31

#d30 Source

d30 :: NProxy D30

#d3 Source

d3 :: NProxy D3

#d29 Source

d29 :: NProxy D29

#d28 Source

d28 :: NProxy D28

#d27 Source

d27 :: NProxy D27

#d26 Source

d26 :: NProxy D26

#d25 Source

d25 :: NProxy D25

#d24 Source

d24 :: NProxy D24

#d23 Source

d23 :: NProxy D23

#d22 Source

d22 :: NProxy D22

#d21 Source

d21 :: NProxy D21

#d20 Source

d20 :: NProxy D20

#d2 Source

d2 :: NProxy D2

#d19 Source

d19 :: NProxy D19

#d18 Source

d18 :: NProxy D18

#d17 Source

d17 :: NProxy D17

#d16 Source

d16 :: NProxy D16

#d15 Source

d15 :: NProxy D15

#d14 Source

d14 :: NProxy D14

#d13 Source

d13 :: NProxy D13

#d12 Source

d12 :: NProxy D12

#d11 Source

d11 :: NProxy D11

#d100 Source

d100 :: NProxy D100

#d10 Source

d10 :: NProxy D10

#d1 Source

d1 :: NProxy D1

#d0 Source

d0 :: NProxy 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