Module

Type.Data.Peano.Nat.Definition

#Nat 

data Nat

Represents a non-negative whole Number ℕ₀

#Z 

data Z :: Nat

Represents 0

Instances

#Succ 

data Succ :: Nat -> Nat

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

Instances

#NProxy 

data NProxy (n :: Nat)

Constructors

Instances

#IsNat 

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

#showNat 

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

#SumNat 

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

a + b = c

Instances

#plusNat 

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

#ProductNat 

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

a * b = c

Instances

#mulNat 

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

#ExponentiationNat 

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

Instances

#powNat 

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 

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

Instances

#IsZeroNat 

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

Instances

#Pred 

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

Instances

#pred 

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

Modules