add natural exponentiation

2016-11-28 21:14:14 +01:00 · 2016-11-28 21:14:14 +01:00 · 0994ae2940
commit 0994ae2940
parent f0b2422711
1 changed files with 5 additions and 0 deletions
--- 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