on master help sign in
Added natural number exponentials
commita9c55de1702c13bc0d10f51ae0f6833fcad339fd authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateThu 9 May 2013, 22:04 (13 years ago) parente534f8a
1 file changed+4
lib/Prelude.idr+4
lib/Prelude.idr+4
@@ -148,6 +148,10 @@ instance Monad List where
148148%include "math.h"
149149%lib "m"
150150
151+pow : (Num a) => a -> Nat -> a
152+pow x O = 1
153+pow x (S n) = x * (pow x n)
154+
151155exp : Float -> Float
152156exp x = prim__floatExp x
153157