Module

Type.Data.Peano

Re-exports from Type.Data.Peano.Int

#Pos

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

type P99 = Pos D99

#P98

type P98 = Pos D98

#P97

type P97 = Pos D97

#P96

type P96 = Pos D96

#P95

type P95 = Pos D95

#P94

type P94 = Pos D94

#P93

type P93 = Pos D93

#P92

type P92 = Pos D92

#P91

type P91 = Pos D91

#P90

type P90 = Pos D90

#P9

type P9 = Pos D9

#P89

type P89 = Pos D89

#P88

type P88 = Pos D88

#P87

type P87 = Pos D87

#P86

type P86 = Pos D86

#P85

type P85 = Pos D85

#P84

type P84 = Pos D84

#P83

type P83 = Pos D83

#P82

type P82 = Pos D82

#P81

type P81 = Pos D81

#P80

type P80 = Pos D80

#P8

type P8 = Pos D8

#P79

type P79 = Pos D79

#P78

type P78 = Pos D78

#P77

type P77 = Pos D77

#P76

type P76 = Pos D76

#P75

type P75 = Pos D75

#P74

type P74 = Pos D74

#P73

type P73 = Pos D73

#P72

type P72 = Pos D72

#P71

type P71 = Pos D71

#P70

type P70 = Pos D70

#P7

type P7 = Pos D7

#P69

type P69 = Pos D69

#P68

type P68 = Pos D68

#P67

type P67 = Pos D67

#P66

type P66 = Pos D66

#P65

type P65 = Pos D65

#P64

type P64 = Pos D64

#P63

type P63 = Pos D63

#P62

type P62 = Pos D62

#P61

type P61 = Pos D61

#P60

type P60 = Pos D60

#P6

type P6 = Pos D6

#P59

type P59 = Pos D59

#P58

type P58 = Pos D58

#P57

type P57 = Pos D57

#P56

type P56 = Pos D56

#P55

type P55 = Pos D55

#P54

type P54 = Pos D54

#P53

type P53 = Pos D53

#P52

type P52 = Pos D52

#P51

type P51 = Pos D51

#P50

type P50 = Pos D50

#P5

type P5 = Pos D5

#P49

type P49 = Pos D49

#P48

type P48 = Pos D48

#P47

type P47 = Pos D47

#P46

type P46 = Pos D46

#P45

type P45 = Pos D45

#P44

type P44 = Pos D44

#P43

type P43 = Pos D43

#P42

type P42 = Pos D42

#P41

type P41 = Pos D41

#P40

type P40 = Pos D40

#P4

type P4 = Pos D4

#P39

type P39 = Pos D39

#P38

type P38 = Pos D38

#P37

type P37 = Pos D37

#P36

type P36 = Pos D36

#P35

type P35 = Pos D35

#P34

type P34 = Pos D34

#P33

type P33 = Pos D33

#P32

type P32 = Pos D32

#P31

type P31 = Pos D31

#P30

type P30 = Pos D30

#P3

type P3 = Pos D3

#P29

type P29 = Pos D29

#P28

type P28 = Pos D28

#P27

type P27 = Pos D27

#P26

type P26 = Pos D26

#P25

type P25 = Pos D25

#P24

type P24 = Pos D24

#P23

type P23 = Pos D23

#P22

type P22 = Pos D22

#P21

type P21 = Pos D21

#P20

type P20 = Pos D20

#P2

type P2 = Pos D2

#P19

type P19 = Pos D19

#P18

type P18 = Pos D18

#P17

type P17 = Pos D17

#P16

type P16 = Pos D16

#P15

type P15 = Pos D15

#P14

type P14 = Pos D14

#P13

type P13 = Pos D13

#P12

type P12 = Pos D12

#P11

type P11 = Pos D11

#P100

type P100 = Pos D100

#P10

type P10 = Pos D10

#P1

type P1 = Pos D1

#P0

type P0 = Pos D0

#Neg

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

type N99 = Neg D99

#N98

type N98 = Neg D98

#N97

type N97 = Neg D97

#N96

type N96 = Neg D96

#N95

type N95 = Neg D95

#N94

type N94 = Neg D94

#N93

type N93 = Neg D93

#N92

type N92 = Neg D92

#N91

type N91 = Neg D91

#N90

type N90 = Neg D90

#N9

type N9 = Neg D9

#N89

type N89 = Neg D89

#N88

type N88 = Neg D88

#N87

type N87 = Neg D87

#N86

type N86 = Neg D86

#N85

type N85 = Neg D85

#N84

type N84 = Neg D84

#N83

type N83 = Neg D83

#N82

type N82 = Neg D82

#N81

type N81 = Neg D81

#N80

type N80 = Neg D80

#N8

type N8 = Neg D8

#N79

type N79 = Neg D79

#N78

type N78 = Neg D78

#N77

type N77 = Neg D77

#N76

type N76 = Neg D76

#N75

type N75 = Neg D75

#N74

type N74 = Neg D74

#N73

type N73 = Neg D73

#N72

type N72 = Neg D72

#N71

type N71 = Neg D71

#N70

type N70 = Neg D70

#N7

type N7 = Neg D7

#N69

type N69 = Neg D69

#N68

type N68 = Neg D68

#N67

type N67 = Neg D67

#N66

type N66 = Neg D66

#N65

type N65 = Neg D65

#N64

type N64 = Neg D64

#N63

type N63 = Neg D63

#N62

type N62 = Neg D62

#N61

type N61 = Neg D61

#N60

type N60 = Neg D60

#N6

type N6 = Neg D6

#N59

type N59 = Neg D59

#N58

type N58 = Neg D58

#N57

type N57 = Neg D57

#N56

type N56 = Neg D56

#N55

type N55 = Neg D55

#N54

type N54 = Neg D54

#N53

type N53 = Neg D53

#N52

type N52 = Neg D52

#N51

type N51 = Neg D51

#N50

type N50 = Neg D50

#N5

type N5 = Neg D5

#N49

type N49 = Neg D49

#N48

type N48 = Neg D48

#N47

type N47 = Neg D47

#N46

type N46 = Neg D46

#N45

type N45 = Neg D45

#N44

type N44 = Neg D44

#N43

type N43 = Neg D43

#N42

type N42 = Neg D42

#N41

type N41 = Neg D41

#N40

type N40 = Neg D40

#N4

type N4 = Neg D4

#N39

type N39 = Neg D39

#N38

type N38 = Neg D38

#N37

type N37 = Neg D37

#N36

type N36 = Neg D36

#N35

type N35 = Neg D35

#N34

type N34 = Neg D34

#N33

type N33 = Neg D33

#N32

type N32 = Neg D32

#N31

type N31 = Neg D31

#N30

type N30 = Neg D30

#N3

type N3 = Neg D3

#N29

type N29 = Neg D29

#N28

type N28 = Neg D28

#N27

type N27 = Neg D27

#N26

type N26 = Neg D26

#N25

type N25 = Neg D25

#N24

type N24 = Neg D24

#N23

type N23 = Neg D23

#N22

type N22 = Neg D22

#N21

type N21 = Neg D21

#N20

type N20 = Neg D20

#N2

type N2 = Neg D2

#N19

type N19 = Neg D19

#N18

type N18 = Neg D18

#N17

type N17 = Neg D17

#N16

type N16 = Neg D16

#N15

type N15 = Neg D15

#N14

type N14 = Neg D14

#N13

type N13 = Neg D13

#N12

type N12 = Neg D12

#N11

type N11 = Neg D11

#N100

type N100 = Neg D100

#N10

type N10 = Neg D10

#N1

type N1 = Neg D1

#N0

type N0 = Neg D0

#Int

data Int

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

#IProxy

data IProxy (i :: Int)

Constructors

IProxy

Instances

(IsInt i) => Show (IProxy i)

#Inverse

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

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

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

Instances

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

#ParseInt

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

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

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

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

#prod

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

#plus

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

#parseInt

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

p99 :: forall proxy. proxy P99

#p98

p98 :: forall proxy. proxy P98

#p97

p97 :: forall proxy. proxy P97

#p96

p96 :: forall proxy. proxy P96

#p95

p95 :: forall proxy. proxy P95

#p94

p94 :: forall proxy. proxy P94

#p93

p93 :: forall proxy. proxy P93

#p92

p92 :: forall proxy. proxy P92

#p91

p91 :: forall proxy. proxy P91

#p90

p90 :: forall proxy. proxy P90

#p9

p9 :: forall proxy. proxy P9

#p89

p89 :: forall proxy. proxy P89

#p88

p88 :: forall proxy. proxy P88

#p87

p87 :: forall proxy. proxy P87

#p86

p86 :: forall proxy. proxy P86

#p85

p85 :: forall proxy. proxy P85

#p84

p84 :: forall proxy. proxy P84

#p83

p83 :: forall proxy. proxy P83

#p82

p82 :: forall proxy. proxy P82

#p81

p81 :: forall proxy. proxy P81

#p80

p80 :: forall proxy. proxy P80

#p8

p8 :: forall proxy. proxy P8

#p79

p79 :: forall proxy. proxy P79

#p78

p78 :: forall proxy. proxy P78

#p77

p77 :: forall proxy. proxy P77

#p76

p76 :: forall proxy. proxy P76

#p75

p75 :: forall proxy. proxy P75

#p74

p74 :: forall proxy. proxy P74

#p73

p73 :: forall proxy. proxy P73

#p72

p72 :: forall proxy. proxy P72

#p71

p71 :: forall proxy. proxy P71

#p70

p70 :: forall proxy. proxy P70

#p7

p7 :: forall proxy. proxy P7

#p69

p69 :: forall proxy. proxy P69

#p68

p68 :: forall proxy. proxy P68

#p67

p67 :: forall proxy. proxy P67

#p66

p66 :: forall proxy. proxy P66

#p65

p65 :: forall proxy. proxy P65

#p64

p64 :: forall proxy. proxy P64

#p63

p63 :: forall proxy. proxy P63

#p62

p62 :: forall proxy. proxy P62

#p61

p61 :: forall proxy. proxy P61

#p60

p60 :: forall proxy. proxy P60

#p6

p6 :: forall proxy. proxy P6

#p59

p59 :: forall proxy. proxy P59

#p58

p58 :: forall proxy. proxy P58

#p57

p57 :: forall proxy. proxy P57

#p56

p56 :: forall proxy. proxy P56

#p55

p55 :: forall proxy. proxy P55

#p54

p54 :: forall proxy. proxy P54

#p53

p53 :: forall proxy. proxy P53

#p52

p52 :: forall proxy. proxy P52

#p51

p51 :: forall proxy. proxy P51

#p50

p50 :: forall proxy. proxy P50

#p5

p5 :: forall proxy. proxy P5

#p49

p49 :: forall proxy. proxy P49

#p48

p48 :: forall proxy. proxy P48

#p47

p47 :: forall proxy. proxy P47

#p46

p46 :: forall proxy. proxy P46

#p45

p45 :: forall proxy. proxy P45

#p44

p44 :: forall proxy. proxy P44

#p43

p43 :: forall proxy. proxy P43

#p42

p42 :: forall proxy. proxy P42

#p41

p41 :: forall proxy. proxy P41

#p40

p40 :: forall proxy. proxy P40

#p4

p4 :: forall proxy. proxy P4

#p39

p39 :: forall proxy. proxy P39

#p38

p38 :: forall proxy. proxy P38

#p37

p37 :: forall proxy. proxy P37

#p36

p36 :: forall proxy. proxy P36

#p35

p35 :: forall proxy. proxy P35

#p34

p34 :: forall proxy. proxy P34

#p33

p33 :: forall proxy. proxy P33

#p32

p32 :: forall proxy. proxy P32

#p31

p31 :: forall proxy. proxy P31

#p30

p30 :: forall proxy. proxy P30

#p3

p3 :: forall proxy. proxy P3

#p29

p29 :: forall proxy. proxy P29

#p28

p28 :: forall proxy. proxy P28

#p27

p27 :: forall proxy. proxy P27

#p26

p26 :: forall proxy. proxy P26

#p25

p25 :: forall proxy. proxy P25

#p24

p24 :: forall proxy. proxy P24

#p23

p23 :: forall proxy. proxy P23

#p22

p22 :: forall proxy. proxy P22

#p21

p21 :: forall proxy. proxy P21

#p20

p20 :: forall proxy. proxy P20

#p2

p2 :: forall proxy. proxy P2

#p19

p19 :: forall proxy. proxy P19

#p18

p18 :: forall proxy. proxy P18

#p17

p17 :: forall proxy. proxy P17

#p16

p16 :: forall proxy. proxy P16

#p15

p15 :: forall proxy. proxy P15

#p14

p14 :: forall proxy. proxy P14

#p13

p13 :: forall proxy. proxy P13

#p12

p12 :: forall proxy. proxy P12

#p11

p11 :: forall proxy. proxy P11

#p100

p100 :: forall proxy. proxy P100

#p10

p10 :: forall proxy. proxy P10

#p1

p1 :: forall proxy. proxy P1

#p0

p0 :: forall proxy. proxy P0

#n99

n99 :: forall proxy. proxy N99

#n98

n98 :: forall proxy. proxy N98

#n97

n97 :: forall proxy. proxy N97

#n96

n96 :: forall proxy. proxy N96

#n95

n95 :: forall proxy. proxy N95

#n94

n94 :: forall proxy. proxy N94

#n93

n93 :: forall proxy. proxy N93

#n92

n92 :: forall proxy. proxy N92

#n91

n91 :: forall proxy. proxy N91

#n90

n90 :: forall proxy. proxy N90

#n9

n9 :: forall proxy. proxy N9

#n89

n89 :: forall proxy. proxy N89

#n88

n88 :: forall proxy. proxy N88

#n87

n87 :: forall proxy. proxy N87

#n86

n86 :: forall proxy. proxy N86

#n85

n85 :: forall proxy. proxy N85

#n84

n84 :: forall proxy. proxy N84

#n83

n83 :: forall proxy. proxy N83

#n82

n82 :: forall proxy. proxy N82

#n81

n81 :: forall proxy. proxy N81

#n80

n80 :: forall proxy. proxy N80

#n8

n8 :: forall proxy. proxy N8

#n79

n79 :: forall proxy. proxy N79

#n78

n78 :: forall proxy. proxy N78

#n77

n77 :: forall proxy. proxy N77

#n76

n76 :: forall proxy. proxy N76

#n75

n75 :: forall proxy. proxy N75

#n74

n74 :: forall proxy. proxy N74

#n73

n73 :: forall proxy. proxy N73

#n72

n72 :: forall proxy. proxy N72

#n71

n71 :: forall proxy. proxy N71

#n70

n70 :: forall proxy. proxy N70

#n7

n7 :: forall proxy. proxy N7

#n69

n69 :: forall proxy. proxy N69

#n68

n68 :: forall proxy. proxy N68

#n67

n67 :: forall proxy. proxy N67

#n66

n66 :: forall proxy. proxy N66

#n65

n65 :: forall proxy. proxy N65

#n64

n64 :: forall proxy. proxy N64

#n63

n63 :: forall proxy. proxy N63

#n62

n62 :: forall proxy. proxy N62

#n61

n61 :: forall proxy. proxy N61

#n60

n60 :: forall proxy. proxy N60

#n6

n6 :: forall proxy. proxy N6

#n59

n59 :: forall proxy. proxy N59

#n58

n58 :: forall proxy. proxy N58

#n57

n57 :: forall proxy. proxy N57

#n56

n56 :: forall proxy. proxy N56

#n55

n55 :: forall proxy. proxy N55

#n54

n54 :: forall proxy. proxy N54

#n53

n53 :: forall proxy. proxy N53

#n52

n52 :: forall proxy. proxy N52

#n51

n51 :: forall proxy. proxy N51

#n50

n50 :: forall proxy. proxy N50

#n5

n5 :: forall proxy. proxy N5

#n49

n49 :: forall proxy. proxy N49

#n48

n48 :: forall proxy. proxy N48

#n47

n47 :: forall proxy. proxy N47

#n46

n46 :: forall proxy. proxy N46

#n45

n45 :: forall proxy. proxy N45

#n44

n44 :: forall proxy. proxy N44

#n43

n43 :: forall proxy. proxy N43

#n42

n42 :: forall proxy. proxy N42

#n41

n41 :: forall proxy. proxy N41

#n40

n40 :: forall proxy. proxy N40

#n4

n4 :: forall proxy. proxy N4

#n39

n39 :: forall proxy. proxy N39

#n38

n38 :: forall proxy. proxy N38

#n37

n37 :: forall proxy. proxy N37

#n36

n36 :: forall proxy. proxy N36

#n35

n35 :: forall proxy. proxy N35

#n34

n34 :: forall proxy. proxy N34

#n33

n33 :: forall proxy. proxy N33

#n32

n32 :: forall proxy. proxy N32

#n31

n31 :: forall proxy. proxy N31

#n30

n30 :: forall proxy. proxy N30

#n3

n3 :: forall proxy. proxy N3

#n29

n29 :: forall proxy. proxy N29

#n28

n28 :: forall proxy. proxy N28

#n27

n27 :: forall proxy. proxy N27

#n26

n26 :: forall proxy. proxy N26

#n25

n25 :: forall proxy. proxy N25

#n24

n24 :: forall proxy. proxy N24

#n23

n23 :: forall proxy. proxy N23

#n22

n22 :: forall proxy. proxy N22

#n21

n21 :: forall proxy. proxy N21

#n20

n20 :: forall proxy. proxy N20

#n2

n2 :: forall proxy. proxy N2

#n19

n19 :: forall proxy. proxy N19

#n18

n18 :: forall proxy. proxy N18

#n17

n17 :: forall proxy. proxy N17

#n16

n16 :: forall proxy. proxy N16

#n15

n15 :: forall proxy. proxy N15

#n14

n14 :: forall proxy. proxy N14

#n13

n13 :: forall proxy. proxy N13

#n12

n12 :: forall proxy. proxy N12

#n11

n11 :: forall proxy. proxy N11

#n100

n100 :: forall proxy. proxy N100

#n10

n10 :: forall proxy. proxy N10

#n1

n1 :: forall proxy. proxy N1

#n0

n0 :: forall proxy. proxy N0

Re-exports from Type.Data.Peano.Nat

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

#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

#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

#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

#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

#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

#mulNat

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

#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