Encoding of ordinals up to epsilon_0 as an iterated multiset: definition in Basic Proof Theory by Troelstra and Schwichenberg. Note, this is not the most efficient way to calculate ordinals. This library is better than having none. I think CNF representation would be more efficent, planning to add in the next version of this library.

For further analysis on efficiency of implementations on ordinals see http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.8089

FYI, an ordinal calculator that covers wider range beyond epsion_0 can be found at http://www.mtnmath.com/ord/ which is written C++. However, I found a serious error in this calculator (ver 0.2): the property a^b * a^c == a^(b+c) does not hold. For example,

ordCalc> 3 ^(w^w + w + 1) * 3^(w^w) == 3 ^ (w^w + w + 1 + w^w) FALSE

This calculator didn't seem to run QuickCeck style automatic testing, although it does have hundreds (or maybe more than a thousand) tests cases but some of them even causes segmentation faults depending on the machine I built this ordCalc.

# Types

# Operators

There are more operators such as
`+`

(addition), `*`

(multiplication), `-`

, (left addtion)
defined in the `Num`

class instance declaration for `Ordinal`

.
Although ordinals are not really `Num`

we decided to make it
as a `Num`

instance for convenience; We can use functions such
as `sum`

and `product`

over list of ordinals and they behave well.
We also plan to implement division and remainder operations
in the `Integral`

class instance for similar reason. For further
information on class instances see the source code.

# Auxiliary functions

convenience function that takes an argument as the power of omega (the first limit ordinal).