# hub.darcs.net :: vmchale -> lazy_matrices -> files

Matrix math in Idris

## root / Test / Spec.idr

 ```1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 ``` ``````module Test.Spec import Specdris.Spec import Data.Fin import Data.Matrix import Data.Vect import Control.Permutation total simple : Matrix 1 Int simple = MatrixC go where go : Fin 2 -> Fin 2 -> Int go FZ FZ = 1 go FZ (FS _) = 2 go (FS _) FZ = 3 go (FS _) (FS _) = 4 total simpleI : Matrix 1 Double simpleI = MatrixC go where go : Fin 2 -> Fin 2 -> Double go FZ FZ = 1 go FZ (FS _) = 2 go (FS _) FZ = 3 go (FS _) (FS _) = 4 total boring : Matrix 1 Double boring = MatrixC go where go : Fin 2 -> Fin 2 -> Double go (FS _) (FS _) = 1 go _ _ = 0 complicated : Matrix 2 Int complicated = identity invertible : Matrix 2 Double invertible = identity -- FIXME determinant is reasonably fast, inverse is decidedly not. export specSuite : IO () specSuite = spec \$ do describe "rank" \$ do it "should compute the rank of a matrix" \$ rank boring `shouldBe` FS (FZ) describe "determinant" \$ do it "should yield the correct determinant" \$ det simple `shouldBe` -2 it "should be a homomorphism" \$ det (multiply simple identity) `shouldBe` -2 it "should return 1 for the identity matrix" \$ det complicated `shouldBe` 1 describe "show" \$ it "should pretty-print" \$ show simple `shouldBe` "[[1, 2],\n [3, 4]]" describe "inverse" \$ do it "should be invert the identity matrix" \$ inverse invertible `shouldBe` identity it "should satisfy x⁻¹x=e" \$ multiply (simpleI) (inverse simpleI) `shouldBe` identity``````