# Using Quaternions in Idris

I am experimenting with using the Idris language to implement algebra and proofs in mathematical code. As a test I have attempted to implement quaternions in the code here.

 To run the REPL I created a shell script file called idris.sh with this contents: ```cd Idris-dev/libs/algebra idris -p effects``` This is then run by typing ./idris.sh in the command line: ```mjb@linux:~> ./idris.sh / _/___/ /____(_) / // __ / ___/ / ___/ Version 1.2.0 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Idris is free software with ABSOLUTELY NO WARRANTY. For details type :warranty. Idris> ``` Or use idris hello.idr to compile code: ```\$ idris hello.idr ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Type checking ./hello.idr```

Below is an example session in REPL showing how to use the code.

 ```Type checking ./quaternion.idr Quat 1.0 2.0 0.0 0.0 : Quaternion Double λΠ> :let q1 = 1.0 + i 2.0 defined λΠ> :let q3 = 1.0 + i 2.0 + j 3.0 defined λΠ> :let q4 = q3 + k 4.0 defined λΠ> q4 Quat 1.0 2.0 3.0 4.0 : Quaternion Double λΠ> :let q5 = normalise q4 defined λΠ> q5 Quat 0.18257418583505536 0.3651483716701107 0.5477225575051661 0.7302967433402214 : Quaternion Double λΠ> :let m6 = quaternion2Matrix q5 defined λΠ> m6 [[-0.6666666666666663, 0.13333333333333336, 0.7333333333333332], [0.6666666666666665, -0.33333333333333304, 0.6666666666666666], [0.33333333333333326, 0.9333333333333332, 0.13333333333333353]] : Vect 3 (Vect 3 Double) λΠ> matrix2Quaternion m6 Quat 0.18257418583505597 0.36514837167010944 0.5477225575051642 0.7302967433402189 : Quaternion Double λΠ> ```
 To leave Idris: ```Idris> :q Bye bye mjb@linux:~> ```