Utils.Peano

Can be used to encode natural numbers as types.

Documentation

data Nat

Typelevel Peano numbers.

Constructors

Z

Zero

S Nat

Successor

Instances

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

data SNat n where

Singleton definition for Nat

Constructors

SZ :: SNat Z

SS :: SNat n -> SNat (S n)

derivePeanoAliases

Arguments

:: Integer

X, the maximum decimal type alias.

-> Q [Dec]

Derives type aliases D0, D1, ..., DX, where Da is equivalent to the decimal number a, written as a Peano number.

toInt :: Nat -> Int

Converts a Nat to its Int representation.

toNat :: Int -> Nat

Converts an Int to its Nat representation.