git.iko.soy/Idris-dev
on master help sign in
added hyperoperation sequence
f67b721Mekeor Melire
lib/prelude/nat.idr+8
compare with master
unifiedsplit
@@ -44,6 +44,14 @@ total power : Nat -> Nat -> Nat
44power base O = S O
44power base O = S O
45power base (S exp) = mult base $ power base exp
45power base (S exp) = mult base $ power base exp
46
46
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+
47--------------------------------------------------------------------------------
55--------------------------------------------------------------------------------
48-- Comparisons
56-- Comparisons
49--------------------------------------------------------------------------------
57--------------------------------------------------------------------------------