Safe Haskell | Safe-Infered |
---|

In this module we provide a way to canonically define a totally
ordered set with a given number of elements. These types have a
custom

instances so that their elements are displayed with
usual decimal number.
`Show`

= {`Succ`

`One`

, `First`

} = {1,2}
`Succ`

`One`

= {`Succ`

`Succ`

`One`

, `First`

, `Succ`

`First`

} = {1,2,3}
`Succ`

`Succ`

`One`

...

# Documentation

A set with one element.

If `n`

is a set with n elements,

is a set with n+1 elements.
`Succ`

n

Monad Succ | |

Functor Succ | |

(Ordinal m, Ordinal n, Prod m n, Sum m (:*: m n), Ordinal (:+: m (:*: m n))) => Prod m (Succ n) | |

(Ordinal m, Ordinal n, Ordinal (:+: m n), Sum m n) => Sum m (Succ n) | |

Bounded n => Bounded (Succ n) | |

(Bounded n, Enum n, Ordinal n) => Enum (Succ n) | |

Eq n => Eq (Succ n) | |

Ord n => Ord (Succ n) | |

Ordinal n => Show (Succ n) | |

Cardinality n => Cardinality (Succ n) | |

Ordinal n => Ordinal (Succ n) |

class (Cardinality n, Ord n) => Ordinal n whereSource

Class of ordered sets with n elements. The methods in this class provide a convenient way to convert to and from a numeric type.

module Data.TypeAlgebra