# HG changeset patch # User haftmann # Date 1179424160 -7200 # Node ID d8b4f2dc2b1da6ecd9c9fb729025a34097d01def # Parent 02440636214f8b67e693df17afa07559d93d3709 refined pow function diff -r 02440636214f -r d8b4f2dc2b1d 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;