Module

Type.Data.Peano.Nat.Definition

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

#Nat Source

data Nat :: Type

Represents a non-negative whole Number ℕ₀

#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

#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

#SumNat Source

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

a + b = c

Instances

#plusNat Source

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

#ProductNat Source

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

a * b = c

Instances

#mulNat Source

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

#ExponentiationNat Source

class ExponentiationNat (a :: Nat) (b :: Nat) (c :: Nat) | 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

#CompareNat Source

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

Instances

#IsZeroNat Source

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

Instances