Matrix.idr

module Data.Matrix

Matrix : (m: Nat) -> (n: Nat) -> (a: Type) -> Type
Matrix m n a = Vect m (Vect n a)

madd : Num a => {n : _} -> Matrix m n a -> Matrix m n a -> Matrix m n a
madd [] [] = []
madd (x :: xs) (y :: ys) = vadd {n=n} x y :: madd xs ys
  where
    vadd : {n : _} -> Vect n a -> Vect n a -> Vect n a
    vadd {n=Z} [] [] = []
    vadd {n=(S pred)} (vx :: vxs) (vy :: vys) = (vx + vy) :: vadd {n=pred} vxs vys