Module

Type.Data.Peano.Nat.Definition

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

#Nat Source

data Nat

Represents a non-negative whole Number ℕ₀

#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

#NProxy Source

data NProxy (n :: Nat)

Constructors

NProxy

Instances

(IsNat a) => Show (NProxy a)

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

#showNat Source

showNat :: forall proxy n. IsNat n => proxy n -> String

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

#plusNat Source

plusNat :: forall proxy a b c. SumNat a b c => proxy a -> proxy b -> proxy c

#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

#mulNat Source

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

#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

#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

#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

#IsZeroNat Source

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

Instances

IsZeroNat Z True
IsZeroNat (Succ a) False

#Pred Source

class Pred (a :: Nat) (b :: Nat) | a -> b, b -> a

Instances

Pred (Succ a) a

#pred Source

pred :: forall proxy a. (proxy (Succ a)) -> proxy a

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