Module

Type.Data.Peano

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

Re-exports from Type.Data.Peano.Int

#Pos Source

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

Instances

(IsNat n) => IsInt (Pos n)
(SumInt (Pos a) (Pos b) (Pos c')) => SumInt (Pos (Succ a)) (Pos b) (Pos (Succ c'))
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
SumInt (Pos Z) (Pos b) (Pos b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)
Inverse (Pos Z) (Pos Z)
Inverse (Pos a) (Neg a)
Inverse (Neg Z) (Pos Z)
Inverse (Neg a) (Pos a)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
ProductInt (Pos Z) a (Pos Z)
ProductInt (Pos (Succ Z)) a a
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(ProductInt (Pos a) b ab, SumInt ab b result) => ProductInt (Pos (Succ a)) b result
(IsZeroNat a isZero) => IsZeroInt (Pos a) isZero

#P99 Source

type P99 = Pos D99

#P98 Source

type P98 = Pos D98

#P97 Source

type P97 = Pos D97

#P96 Source

type P96 = Pos D96

#P95 Source

type P95 = Pos D95

#P94 Source

type P94 = Pos D94

#P93 Source

type P93 = Pos D93

#P92 Source

type P92 = Pos D92

#P91 Source

type P91 = Pos D91

#P90 Source

type P90 = Pos D90

#P9 Source

type P9 = Pos D9

#P89 Source

type P89 = Pos D89

#P88 Source

type P88 = Pos D88

#P87 Source

type P87 = Pos D87

#P86 Source

type P86 = Pos D86

#P85 Source

type P85 = Pos D85

#P84 Source

type P84 = Pos D84

#P83 Source

type P83 = Pos D83

#P82 Source

type P82 = Pos D82

#P81 Source

type P81 = Pos D81

#P80 Source

type P80 = Pos D80

#P8 Source

type P8 = Pos D8

#P79 Source

type P79 = Pos D79

#P78 Source

type P78 = Pos D78

#P77 Source

type P77 = Pos D77

#P76 Source

type P76 = Pos D76

#P75 Source

type P75 = Pos D75

#P74 Source

type P74 = Pos D74

#P73 Source

type P73 = Pos D73

#P72 Source

type P72 = Pos D72

#P71 Source

type P71 = Pos D71

#P70 Source

type P70 = Pos D70

#P7 Source

type P7 = Pos D7

#P69 Source

type P69 = Pos D69

#P68 Source

type P68 = Pos D68

#P67 Source

type P67 = Pos D67

#P66 Source

type P66 = Pos D66

#P65 Source

type P65 = Pos D65

#P64 Source

type P64 = Pos D64

#P63 Source

type P63 = Pos D63

#P62 Source

type P62 = Pos D62

#P61 Source

type P61 = Pos D61

#P60 Source

type P60 = Pos D60

#P6 Source

type P6 = Pos D6

#P59 Source

type P59 = Pos D59

#P58 Source

type P58 = Pos D58

#P57 Source

type P57 = Pos D57

#P56 Source

type P56 = Pos D56

#P55 Source

type P55 = Pos D55

#P54 Source

type P54 = Pos D54

#P53 Source

type P53 = Pos D53

#P52 Source

type P52 = Pos D52

#P51 Source

type P51 = Pos D51

#P50 Source

type P50 = Pos D50

#P5 Source

type P5 = Pos D5

#P49 Source

type P49 = Pos D49

#P48 Source

type P48 = Pos D48

#P47 Source

type P47 = Pos D47

#P46 Source

type P46 = Pos D46

#P45 Source

type P45 = Pos D45

#P44 Source

type P44 = Pos D44

#P43 Source

type P43 = Pos D43

#P42 Source

type P42 = Pos D42

#P41 Source

type P41 = Pos D41

#P40 Source

type P40 = Pos D40

#P4 Source

type P4 = Pos D4

#P39 Source

type P39 = Pos D39

#P38 Source

type P38 = Pos D38

#P37 Source

type P37 = Pos D37

#P36 Source

type P36 = Pos D36

#P35 Source

type P35 = Pos D35

#P34 Source

type P34 = Pos D34

#P33 Source

type P33 = Pos D33

#P32 Source

type P32 = Pos D32

#P31 Source

type P31 = Pos D31

#P30 Source

type P30 = Pos D30

#P3 Source

type P3 = Pos D3

#P29 Source

type P29 = Pos D29

#P28 Source

type P28 = Pos D28

#P27 Source

type P27 = Pos D27

#P26 Source

type P26 = Pos D26

#P25 Source

type P25 = Pos D25

#P24 Source

type P24 = Pos D24

#P23 Source

type P23 = Pos D23

#P22 Source

type P22 = Pos D22

#P21 Source

type P21 = Pos D21

#P20 Source

type P20 = Pos D20

#P2 Source

type P2 = Pos D2

#P19 Source

type P19 = Pos D19

#P18 Source

type P18 = Pos D18

#P17 Source

type P17 = Pos D17

#P16 Source

type P16 = Pos D16

#P15 Source

type P15 = Pos D15

#P14 Source

type P14 = Pos D14

#P13 Source

type P13 = Pos D13

#P12 Source

type P12 = Pos D12

#P11 Source

type P11 = Pos D11

#P100 Source

type P100 = Pos D100

#P10 Source

type P10 = Pos D10

#P1 Source

type P1 = Pos D1

#P0 Source

type P0 = Pos D0

#Neg Source

data Neg :: Nat -> Int

Represents a negative number

Neg (Succ Z) ^= - 1

Instances

(IsNat n) => IsInt (Neg n)
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
(SumInt (Neg a) (Neg b) (Neg c')) => SumInt (Neg (Succ a)) (Neg b) (Neg (Succ c'))
SumInt (Neg Z) (Neg b) (Neg b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)
Inverse (Pos a) (Neg a)
Inverse (Neg Z) (Pos Z)
Inverse (Neg a) (Pos a)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(IsZeroNat a isZero) => IsZeroInt (Neg a) isZero

#N99 Source

type N99 = Neg D99

#N98 Source

type N98 = Neg D98

#N97 Source

type N97 = Neg D97

#N96 Source

type N96 = Neg D96

#N95 Source

type N95 = Neg D95

#N94 Source

type N94 = Neg D94

#N93 Source

type N93 = Neg D93

#N92 Source

type N92 = Neg D92

#N91 Source

type N91 = Neg D91

#N90 Source

type N90 = Neg D90

#N9 Source

type N9 = Neg D9

#N89 Source

type N89 = Neg D89

#N88 Source

type N88 = Neg D88

#N87 Source

type N87 = Neg D87

#N86 Source

type N86 = Neg D86

#N85 Source

type N85 = Neg D85

#N84 Source

type N84 = Neg D84

#N83 Source

type N83 = Neg D83

#N82 Source

type N82 = Neg D82

#N81 Source

type N81 = Neg D81

#N80 Source

type N80 = Neg D80

#N8 Source

type N8 = Neg D8

#N79 Source

type N79 = Neg D79

#N78 Source

type N78 = Neg D78

#N77 Source

type N77 = Neg D77

#N76 Source

type N76 = Neg D76

#N75 Source

type N75 = Neg D75

#N74 Source

type N74 = Neg D74

#N73 Source

type N73 = Neg D73

#N72 Source

type N72 = Neg D72

#N71 Source

type N71 = Neg D71

#N70 Source

type N70 = Neg D70

#N7 Source

type N7 = Neg D7

#N69 Source

type N69 = Neg D69

#N68 Source

type N68 = Neg D68

#N67 Source

type N67 = Neg D67

#N66 Source

type N66 = Neg D66

#N65 Source

type N65 = Neg D65

#N64 Source

type N64 = Neg D64

#N63 Source

type N63 = Neg D63

#N62 Source

type N62 = Neg D62

#N61 Source

type N61 = Neg D61

#N60 Source

type N60 = Neg D60

#N6 Source

type N6 = Neg D6

#N59 Source

type N59 = Neg D59

#N58 Source

type N58 = Neg D58

#N57 Source

type N57 = Neg D57

#N56 Source

type N56 = Neg D56

#N55 Source

type N55 = Neg D55

#N54 Source

type N54 = Neg D54

#N53 Source

type N53 = Neg D53

#N52 Source

type N52 = Neg D52

#N51 Source

type N51 = Neg D51

#N50 Source

type N50 = Neg D50

#N5 Source

type N5 = Neg D5

#N49 Source

type N49 = Neg D49

#N48 Source

type N48 = Neg D48

#N47 Source

type N47 = Neg D47

#N46 Source

type N46 = Neg D46

#N45 Source

type N45 = Neg D45

#N44 Source

type N44 = Neg D44

#N43 Source

type N43 = Neg D43

#N42 Source

type N42 = Neg D42

#N41 Source

type N41 = Neg D41

#N40 Source

type N40 = Neg D40

#N4 Source

type N4 = Neg D4

#N39 Source

type N39 = Neg D39

#N38 Source

type N38 = Neg D38

#N37 Source

type N37 = Neg D37

#N36 Source

type N36 = Neg D36

#N35 Source

type N35 = Neg D35

#N34 Source

type N34 = Neg D34

#N33 Source

type N33 = Neg D33

#N32 Source

type N32 = Neg D32

#N31 Source

type N31 = Neg D31

#N30 Source

type N30 = Neg D30

#N3 Source

type N3 = Neg D3

#N29 Source

type N29 = Neg D29

#N28 Source

type N28 = Neg D28

#N27 Source

type N27 = Neg D27

#N26 Source

type N26 = Neg D26

#N25 Source

type N25 = Neg D25

#N24 Source

type N24 = Neg D24

#N23 Source

type N23 = Neg D23

#N22 Source

type N22 = Neg D22

#N21 Source

type N21 = Neg D21

#N20 Source

type N20 = Neg D20

#N2 Source

type N2 = Neg D2

#N19 Source

type N19 = Neg D19

#N18 Source

type N18 = Neg D18

#N17 Source

type N17 = Neg D17

#N16 Source

type N16 = Neg D16

#N15 Source

type N15 = Neg D15

#N14 Source

type N14 = Neg D14

#N13 Source

type N13 = Neg D13

#N12 Source

type N12 = Neg D12

#N11 Source

type N11 = Neg D11

#N100 Source

type N100 = Neg D100

#N10 Source

type N10 = Neg D10

#N1 Source

type N1 = Neg D1

#N0 Source

type N0 = Neg D0

#Int Source

data Int

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

#IProxy Source

data IProxy (i :: Int)

Constructors

IProxy

Instances

(IsInt i) => Show (IProxy i)

#Inverse Source

class Inverse (a :: Int) (b :: Int) | a -> b, b -> a

Invert the sign of a value (except for 0, which always stays positive)

Inverse (Pos (Succ Z)) ~> Neg (Succ Z)
Inverse (Pos Z) ~> Pos Z

Instances

Inverse (Pos Z) (Pos Z)
Inverse (Pos a) (Neg a)
Inverse (Neg Z) (Pos Z)
Inverse (Neg a) (Pos a)

#IsInt Source

class IsInt (i :: Int)  where

Members

reflectInt :: forall proxy. proxy i -> Int
reflect a type-level Int to a value-level Int
```
reflectInt (Proxy  :: _ N10) = -10
reflectInt (IProxy :: _ N10) = -10
```

Instances

(IsNat n) => IsInt (Pos n)
(IsNat n) => IsInt (Neg n)

#IsZeroInt Source

class IsZeroInt (int :: Int) (isZero :: Boolean) | int -> isZero

Instances

(IsZeroNat a isZero) => IsZeroInt (Pos a) isZero
(IsZeroNat a isZero) => IsZeroInt (Neg a) isZero

#ParseInt Source

class ParseInt (sym :: Symbol) (int :: Int) | int -> sym, sym -> int

Parse a Int from a Symbol

ParseInt "-10" N10
ParseInt "1337" P1337 -- P1137 would be type alias for Pos (Succ^1337 Z)

Instances

(Equals "-" head isMinus, If isMinus (proxy (Neg natValue)) (proxy (Pos natValue)) (proxy int), If isMinus (sproxy tail) (sproxy sym) (sproxy numberSymbol), Cons head tail sym, ParseNat numberSymbol natValue) => ParseInt sym int

#ProductInt Source

class ProductInt (a :: Int) (b :: Int) (c :: Int) | a b -> c

Instances

(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
ProductInt (Pos Z) a (Pos Z)
ProductInt (Pos (Succ Z)) a a
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(ProductInt (Pos a) b ab, SumInt ab b result) => ProductInt (Pos (Succ a)) b result

#SumInt Source

class SumInt (a :: Int) (b :: Int) (c :: Int) | a b -> c

Instances

(SumInt (Pos a) (Pos b) (Pos c')) => SumInt (Pos (Succ a)) (Pos b) (Pos (Succ c'))
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
(SumInt (Neg a) (Neg b) (Neg c')) => SumInt (Neg (Succ a)) (Neg b) (Neg (Succ c'))
SumInt (Pos Z) (Pos b) (Pos b)
SumInt (Neg Z) (Neg b) (Neg b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)

#showInt Source

showInt :: forall proxy i. IsInt i => proxy i -> String

#prod Source

prod :: forall proxy a b c. ProductInt a b c => proxy a -> proxy b -> proxy c

#plus Source

plus :: forall proxy a b c. SumInt a b c => proxy a -> proxy b -> proxy c

#parseInt Source

parseInt :: forall sproxy proxy sym a. ParseInt sym a => sproxy sym -> proxy a

parse Int a Value-Level

parseInt (Proxy  :: _ "-1337") ~> N1337
parseInt (SProxy :: _ "-1337") ~> N1337
    -- N1137 would be type alias for Neg (Succ^1337 Z)

#p99 Source

p99 :: forall proxy. proxy P99

#p98 Source

p98 :: forall proxy. proxy P98

#p97 Source

p97 :: forall proxy. proxy P97

#p96 Source

p96 :: forall proxy. proxy P96

#p95 Source

p95 :: forall proxy. proxy P95

#p94 Source

p94 :: forall proxy. proxy P94

#p93 Source

p93 :: forall proxy. proxy P93

#p92 Source

p92 :: forall proxy. proxy P92

#p91 Source

p91 :: forall proxy. proxy P91

#p90 Source

p90 :: forall proxy. proxy P90

#p9 Source

p9 :: forall proxy. proxy P9

#p89 Source

p89 :: forall proxy. proxy P89

#p88 Source

p88 :: forall proxy. proxy P88

#p87 Source

p87 :: forall proxy. proxy P87

#p86 Source

p86 :: forall proxy. proxy P86

#p85 Source

p85 :: forall proxy. proxy P85

#p84 Source

p84 :: forall proxy. proxy P84

#p83 Source

p83 :: forall proxy. proxy P83

#p82 Source

p82 :: forall proxy. proxy P82

#p81 Source

p81 :: forall proxy. proxy P81

#p80 Source

p80 :: forall proxy. proxy P80

#p8 Source

p8 :: forall proxy. proxy P8

#p79 Source

p79 :: forall proxy. proxy P79

#p78 Source

p78 :: forall proxy. proxy P78

#p77 Source

p77 :: forall proxy. proxy P77

#p76 Source

p76 :: forall proxy. proxy P76

#p75 Source

p75 :: forall proxy. proxy P75

#p74 Source

p74 :: forall proxy. proxy P74

#p73 Source

p73 :: forall proxy. proxy P73

#p72 Source

p72 :: forall proxy. proxy P72

#p71 Source

p71 :: forall proxy. proxy P71

#p70 Source

p70 :: forall proxy. proxy P70

#p7 Source

p7 :: forall proxy. proxy P7

#p69 Source

p69 :: forall proxy. proxy P69

#p68 Source

p68 :: forall proxy. proxy P68

#p67 Source

p67 :: forall proxy. proxy P67

#p66 Source

p66 :: forall proxy. proxy P66

#p65 Source

p65 :: forall proxy. proxy P65

#p64 Source

p64 :: forall proxy. proxy P64

#p63 Source

p63 :: forall proxy. proxy P63

#p62 Source

p62 :: forall proxy. proxy P62

#p61 Source

p61 :: forall proxy. proxy P61

#p60 Source

p60 :: forall proxy. proxy P60

#p6 Source

p6 :: forall proxy. proxy P6

#p59 Source

p59 :: forall proxy. proxy P59

#p58 Source

p58 :: forall proxy. proxy P58

#p57 Source

p57 :: forall proxy. proxy P57

#p56 Source

p56 :: forall proxy. proxy P56

#p55 Source

p55 :: forall proxy. proxy P55

#p54 Source

p54 :: forall proxy. proxy P54

#p53 Source

p53 :: forall proxy. proxy P53

#p52 Source

p52 :: forall proxy. proxy P52

#p51 Source

p51 :: forall proxy. proxy P51

#p50 Source

p50 :: forall proxy. proxy P50

#p5 Source

p5 :: forall proxy. proxy P5

#p49 Source

p49 :: forall proxy. proxy P49

#p48 Source

p48 :: forall proxy. proxy P48

#p47 Source

p47 :: forall proxy. proxy P47

#p46 Source

p46 :: forall proxy. proxy P46

#p45 Source

p45 :: forall proxy. proxy P45

#p44 Source

p44 :: forall proxy. proxy P44

#p43 Source

p43 :: forall proxy. proxy P43

#p42 Source

p42 :: forall proxy. proxy P42

#p41 Source

p41 :: forall proxy. proxy P41

#p40 Source

p40 :: forall proxy. proxy P40

#p4 Source

p4 :: forall proxy. proxy P4

#p39 Source

p39 :: forall proxy. proxy P39

#p38 Source

p38 :: forall proxy. proxy P38

#p37 Source

p37 :: forall proxy. proxy P37

#p36 Source

p36 :: forall proxy. proxy P36

#p35 Source

p35 :: forall proxy. proxy P35

#p34 Source

p34 :: forall proxy. proxy P34

#p33 Source

p33 :: forall proxy. proxy P33

#p32 Source

p32 :: forall proxy. proxy P32

#p31 Source

p31 :: forall proxy. proxy P31

#p30 Source

p30 :: forall proxy. proxy P30

#p3 Source

p3 :: forall proxy. proxy P3

#p29 Source

p29 :: forall proxy. proxy P29

#p28 Source

p28 :: forall proxy. proxy P28

#p27 Source

p27 :: forall proxy. proxy P27

#p26 Source

p26 :: forall proxy. proxy P26

#p25 Source

p25 :: forall proxy. proxy P25

#p24 Source

p24 :: forall proxy. proxy P24

#p23 Source

p23 :: forall proxy. proxy P23

#p22 Source

p22 :: forall proxy. proxy P22

#p21 Source

p21 :: forall proxy. proxy P21

#p20 Source

p20 :: forall proxy. proxy P20

#p2 Source

p2 :: forall proxy. proxy P2

#p19 Source

p19 :: forall proxy. proxy P19

#p18 Source

p18 :: forall proxy. proxy P18

#p17 Source

p17 :: forall proxy. proxy P17

#p16 Source

p16 :: forall proxy. proxy P16

#p15 Source

p15 :: forall proxy. proxy P15

#p14 Source

p14 :: forall proxy. proxy P14

#p13 Source

p13 :: forall proxy. proxy P13

#p12 Source

p12 :: forall proxy. proxy P12

#p11 Source

p11 :: forall proxy. proxy P11

#p100 Source

p100 :: forall proxy. proxy P100

#p10 Source

p10 :: forall proxy. proxy P10

#p1 Source

p1 :: forall proxy. proxy P1

#p0 Source

p0 :: forall proxy. proxy P0

#n99 Source

n99 :: forall proxy. proxy N99

#n98 Source

n98 :: forall proxy. proxy N98

#n97 Source

n97 :: forall proxy. proxy N97

#n96 Source

n96 :: forall proxy. proxy N96

#n95 Source

n95 :: forall proxy. proxy N95

#n94 Source

n94 :: forall proxy. proxy N94

#n93 Source

n93 :: forall proxy. proxy N93

#n92 Source

n92 :: forall proxy. proxy N92

#n91 Source

n91 :: forall proxy. proxy N91

#n90 Source

n90 :: forall proxy. proxy N90

#n9 Source

n9 :: forall proxy. proxy N9

#n89 Source

n89 :: forall proxy. proxy N89

#n88 Source

n88 :: forall proxy. proxy N88

#n87 Source

n87 :: forall proxy. proxy N87

#n86 Source

n86 :: forall proxy. proxy N86

#n85 Source

n85 :: forall proxy. proxy N85

#n84 Source

n84 :: forall proxy. proxy N84

#n83 Source

n83 :: forall proxy. proxy N83

#n82 Source

n82 :: forall proxy. proxy N82

#n81 Source

n81 :: forall proxy. proxy N81

#n80 Source

n80 :: forall proxy. proxy N80

#n8 Source

n8 :: forall proxy. proxy N8

#n79 Source

n79 :: forall proxy. proxy N79

#n78 Source

n78 :: forall proxy. proxy N78

#n77 Source

n77 :: forall proxy. proxy N77

#n76 Source

n76 :: forall proxy. proxy N76

#n75 Source

n75 :: forall proxy. proxy N75

#n74 Source

n74 :: forall proxy. proxy N74

#n73 Source

n73 :: forall proxy. proxy N73

#n72 Source

n72 :: forall proxy. proxy N72

#n71 Source

n71 :: forall proxy. proxy N71

#n70 Source

n70 :: forall proxy. proxy N70

#n7 Source

n7 :: forall proxy. proxy N7

#n69 Source

n69 :: forall proxy. proxy N69

#n68 Source

n68 :: forall proxy. proxy N68

#n67 Source

n67 :: forall proxy. proxy N67

#n66 Source

n66 :: forall proxy. proxy N66

#n65 Source

n65 :: forall proxy. proxy N65

#n64 Source

n64 :: forall proxy. proxy N64

#n63 Source

n63 :: forall proxy. proxy N63

#n62 Source

n62 :: forall proxy. proxy N62

#n61 Source

n61 :: forall proxy. proxy N61

#n60 Source

n60 :: forall proxy. proxy N60

#n6 Source

n6 :: forall proxy. proxy N6

#n59 Source

n59 :: forall proxy. proxy N59

#n58 Source

n58 :: forall proxy. proxy N58

#n57 Source

n57 :: forall proxy. proxy N57

#n56 Source

n56 :: forall proxy. proxy N56

#n55 Source

n55 :: forall proxy. proxy N55

#n54 Source

n54 :: forall proxy. proxy N54

#n53 Source

n53 :: forall proxy. proxy N53

#n52 Source

n52 :: forall proxy. proxy N52

#n51 Source

n51 :: forall proxy. proxy N51

#n50 Source

n50 :: forall proxy. proxy N50

#n5 Source

n5 :: forall proxy. proxy N5

#n49 Source

n49 :: forall proxy. proxy N49

#n48 Source

n48 :: forall proxy. proxy N48

#n47 Source

n47 :: forall proxy. proxy N47

#n46 Source

n46 :: forall proxy. proxy N46

#n45 Source

n45 :: forall proxy. proxy N45

#n44 Source

n44 :: forall proxy. proxy N44

#n43 Source

n43 :: forall proxy. proxy N43

#n42 Source

n42 :: forall proxy. proxy N42

#n41 Source

n41 :: forall proxy. proxy N41

#n40 Source

n40 :: forall proxy. proxy N40

#n4 Source

n4 :: forall proxy. proxy N4

#n39 Source

n39 :: forall proxy. proxy N39

#n38 Source

n38 :: forall proxy. proxy N38

#n37 Source

n37 :: forall proxy. proxy N37

#n36 Source

n36 :: forall proxy. proxy N36

#n35 Source

n35 :: forall proxy. proxy N35

#n34 Source

n34 :: forall proxy. proxy N34

#n33 Source

n33 :: forall proxy. proxy N33

#n32 Source

n32 :: forall proxy. proxy N32

#n31 Source

n31 :: forall proxy. proxy N31

#n30 Source

n30 :: forall proxy. proxy N30

#n3 Source

n3 :: forall proxy. proxy N3

#n29 Source

n29 :: forall proxy. proxy N29

#n28 Source

n28 :: forall proxy. proxy N28

#n27 Source

n27 :: forall proxy. proxy N27

#n26 Source

n26 :: forall proxy. proxy N26

#n25 Source

n25 :: forall proxy. proxy N25

#n24 Source

n24 :: forall proxy. proxy N24

#n23 Source

n23 :: forall proxy. proxy N23

#n22 Source

n22 :: forall proxy. proxy N22

#n21 Source

n21 :: forall proxy. proxy N21

#n20 Source

n20 :: forall proxy. proxy N20

#n2 Source

n2 :: forall proxy. proxy N2

#n19 Source

n19 :: forall proxy. proxy N19

#n18 Source

n18 :: forall proxy. proxy N18

#n17 Source

n17 :: forall proxy. proxy N17

#n16 Source

n16 :: forall proxy. proxy N16

#n15 Source

n15 :: forall proxy. proxy N15

#n14 Source

n14 :: forall proxy. proxy N14

#n13 Source

n13 :: forall proxy. proxy N13

#n12 Source

n12 :: forall proxy. proxy N12

#n11 Source

n11 :: forall proxy. proxy N11

#n100 Source

n100 :: forall proxy. proxy N100

#n10 Source

n10 :: forall proxy. proxy N10

#n1 Source

n1 :: forall proxy. proxy N1

#n0 Source

n0 :: forall proxy. proxy N0

Re-exports from Type.Data.Peano.Nat

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

#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

#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

#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

#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

#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

#mulNat Source

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

#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