refined pow function
authorhaftmann
Thu, 17 May 2007 19:49:20 +0200
changeset 22995 d8b4f2dc2b1d
parent 22994 02440636214f
child 22996 5f82c5f8478e
refined pow function
src/Pure/General/int.ML
--- a/src/Pure/General/int.ML	Thu May 17 19:49:17 2007 +0200
+++ b/src/Pure/General/int.ML	Thu May 17 19:49:20 2007 +0200
@@ -66,7 +66,16 @@
 nonfix div val div = curry div;
 nonfix mod val mod = curry mod;
 val neg = ~;
-val pow = fn k => fn l => pow (l, toInt k);
+
+fun pow k l =
+  let
+    fun pw 0 = 1
+      | pw k = mult l (pw (sub k 1));
+  in if k < zero
+    then error "pow: negative exponent"
+    else pw k
+  end;
+
 fun exp k = pow k two;
 val log = int o log2;