Module

Type.Data.Peano.Int

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

#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

#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

#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

#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

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

#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

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

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

#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

#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

#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