added hyperoperation sequence
commitf67b7216fbc3672048b363eef5a4ff6bd3172996
authorMekeor Melire <mekeor@ymail.com>
dateMon 4 Jun 2012, 00:01 (14 years ago)
parentc9051be
lib/prelude/nat.idr+8
@@ -44,6 +44,14 @@ total power : Nat -> Nat -> Nat
4444power base O = S O
4545power base (S exp) = mult base $ power base exp
4646
47+hyper : Nat -> Nat -> Nat -> Nat
48+hyper O a b = S b
49+hyper (S O) a O = a
50+hyper (S(S O)) a O = O
51+hyper n a O = S O
52+hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
53+
54+
4755--------------------------------------------------------------------------------
4856-- Comparisons
4957--------------------------------------------------------------------------------