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

#Succ Source

data Succ :: Nat -> Nat

Represents Successor of a Nat: (Succ a) ^= 1 + a

Instances

#NProxy Source

data NProxy (n :: Nat)

Proxy from kind Nat to kind Type

Constructors

Instances

#CompareNat Source

class CompareNat (a :: Nat) (b :: Nat) (ord :: Ordering) | a b -> ord

Instances

#ExponentiationNat Source

class ExponentiationNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

Instances

#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

#IsZeroNat Source

class IsZeroNat (a :: Nat) (isZero :: Boolean) | a -> isZero

Instances

#ProductNat Source

class ProductNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

a * b = c

Instances

#SumNat Source

class SumNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c

a + b = c

Instances

#powNat Source

powNat :: forall c b a. ExponentiationNat a b c => NProxy a -> NProxy b -> NProxy c
> powNat d2 d3
8 -- : NProxy D8

a raised to the power of b a^b = 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 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
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