From 0994ae294011628bf64b7ccba9116033cb979675 Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Mon, 28 Nov 2016 21:14:14 +0100
Subject: [PATCH] add natural exponentiation

---
 src/Data/Nat.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index e53f1aa..95aef0d 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -55,6 +55,11 @@ singletons [d|
   Z     × m = Z
   (S n) × m = (n × m) + m
 
+  -- | Exponentiation
+  (^) ∷ ℕ → ℕ → ℕ
+  n ^ Z     = (S Z)
+  n ^ (S m) = n × (n ^ m)
+
   -- | Ordering relation <
   (<) ∷ ℕ → ℕ → 𝔹
   Z     < Z     = F