on master help sign in
ported Data.Complex from haskell to idris
commit7db77db40b7758ef202eb7211d02a871318361cf authorMekeor Melire <mekeor@ymail.com> dateFri 24 Feb 2012, 14:46 (15 years ago) parentba77a44
1 file changed+36
lib/prelude/complex.idr+36
lib/prelude/complex.idrnew file+36
@@ -0,0 +1,36 @@
1+module prelude.complex
2+
3+import builtins
4+
5+
6+------------------------------ General
7+
8+infix 6 :+
9+data Complex a = (:+) a a
10+
11+realPart : Complex a -> a
12+realPart (r:+i) = r
13+
14+imagPart : Complex a -> a
15+imagPart (r:+i) = i
16+
17+
18+------------------------------ Polarform
19+
20+mkPolar : Float -> Float -> Complex Float
21+mkPolar radius angle = radius * cos angle :+ radius * sin angle
22+
23+cis : Float -> Complex Float
24+cis angle = cos angle :+ sin angle
25+
26+magnitude : Complex Float -> Float
27+magnitude (r:+i) = sqrt (r*r+i*i)
28+
29+phase : Complex Float -> Float
30+phase (x:+y) = atan2 y x
31+
32+
33+------------------------------ Conjugate
34+
35+conjugate : Num a => Complex a -> Complex a
36+conjugate (r:+i) = (r :+ (0-i))