natural-number-1.0: Natural numbers tagged with a type-level representation of the number.

Data.NaturalNumber

Documentation

data N a whereSource

Constructors

NZero :: N Zero
NSuccessorTo :: N n -> N (SuccessorTo n)

Instances

EqT N
Eq (N n)
Show (N n)
NaturalNumber n => Typeable (N n)

data UnknownN whereSource

Constructors

UnknownN :: NaturalNumber n => N n -> UnknownN

Instances

class (NaturalNumber n, Induction n) => NaturalNumber n whereSource

Methods

asN :: N nSource

fromN :: N n -> nSource

Instances

NaturalNumber Zero
NaturalNumber n => NaturalNumber (SuccessorTo n)

nToInt :: N n -> Int Source

unknownNToInt :: UnknownN -> Int Source

intToUnknownN :: Int -> UnknownN Source

intToN :: NaturalNumber n => Int -> N nSource