Type.Data.Peano.Nat.Definition

data Nat :: Type

Represents a non-negative whole Number ℕ₀

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

• CompareNat Z a LT
• CompareNat a Z GT
• IsZeroNat Z True

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
• (CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
• IsZeroNat (Succ a) False

data NProxy (n :: Nat)

Proxy from kind Nat to kind Type

Instances

• (IsNat a) => Show (NProxy a)

class IsNat (a :: Nat)  where

Members

• reflectNat :: NProxy a -> Int

  reflect typelevel Nat to a valuelevel Int

  reflectNat (undefined :: NProxy D10) = 10
  

Instances

• IsNat Z
• (IsNat a) => IsNat (Succ a)

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 :: forall c b a. SumNat a b c => NProxy a -> NProxy b -> NProxy c

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 :: forall c b a. ProductNat a b c => NProxy a -> NProxy b -> NProxy c

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

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

Instances

• IsZeroNat Z True
• IsZeroNat (Succ a) False