Tetration and Hyperoperators

[HalosGhost]

Defining Tetration is trivial (not that it would be practical to use for any but the smallest inputs):

Tetrate = λa.λn.n (Power a) 1;

This may indeed be added to the standard library. However, I am far more interested in the possibility of defining a function Hyper which, when given a natural number, can return the associated hyperoperation, such that Hyper 0 would return a function behaviorally-equivalent to Increment, Hyper 1 would return a function behaviorally-equivalent to Add, etc.

[HalosGhost]

Okay, this is technically completed via eb23b09.

However, this relies on named-recursion. Next step is to define Hyper in terms of a fixpoint combinator. However, the ultimate win would be to implement it without recursion so that it could, hypothetically, be typed.