Module

Type.Data.Peano.Int

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

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

#Pos Source

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

Instances

#Neg Source

data Neg :: Nat -> Int

Represents a negative number

Neg (Succ Z) ^= - 1

Instances

#IProxy Source

data IProxy (i :: Int)

Instances

#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

#IsInt Source

class IsInt (i :: Int)  where

Members

  • reflectInt :: IProxy i -> Int

    reflect a type-level Int to a value-level Int

    reflectInt (undefined :: IProxy N10) = -10
    

Instances

#IsZeroInt Source

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

Instances

#ProductInt Source

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

Instances

#SumInt Source

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

Instances

#prod Source

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

#plus Source

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

#Int Source

kind Int

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

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

#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

#parseInt Source

parseInt :: forall a sym. ParseInt sym a => SProxy sym -> IProxy a

parse Int a Value-Level

parseInt (undefined :: SProxy "-1337") N1337 
    -- N1137 would be type alias for Neg (Succ^1337 Z)

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

#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

#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