n0 = Zero n1 = Suc n0 n2 = Suc n1 n3 = Suc n2 n4 = Suc n3 n5 = Suc n4 n6 = Suc n5 n7 = Suc n6 n8 = Suc n7 n9 = Suc n8 n10 = mul n2 n5 n20 = mul n10 n2 add Zero m = m add (Suc n) m = Suc (add n m) sub Zero _ = Zero sub (Suc n) Zero = Suc n sub (Suc n) (Suc m) = sub n m mul Zero _ = Zero mul (Suc n) m = add m (mul n m) pow n Zero = n1 pow n (Suc m) = mul n (pow n m) divSuc Zero _ = Zero divSuc (Suc n) m = if (less n m) Zero (Suc (divSuc (sub n m) m)) modSuc Zero _ = Zero modSuc (Suc n) m = if (less n m) (Suc n) (modSuc (sub n m) m) div n (Suc m) = divSuc n m mod n (Suc m) = modSuc n m fac Zero = n1 fac (Suc n) = mul (Suc n) (fac n) eq Zero Zero = True eq Zero (Suc _) = False eq (Suc _) Zero = False eq (Suc n) (Suc m) = eq n m if True = \x y -> x if False = \x y -> y less Zero Zero = False less Zero (Suc _) = True less (Suc _) Zero = False less (Suc n) (Suc m) = less n m decimal Zero = \x -> x decimal (Suc n) = (decimal (div (Suc n) n10)) (digit (mod (Suc n) n10)) inc D0 = D1 inc D1 = D2 inc D2 = D3 inc D3 = D4 inc D4 = D5 inc D5 = D6 inc D6 = D7 inc D7 = D8 inc D8 = D9 digit Zero = D0 digit (Suc n) = inc (digit n) main = decimal (add (fac n8) (pow n5 n6)) -- main = decimal (add (fac n6) (pow n3 n7)) -- main = decimal (fac n5)