idris-0.9.9: test/reg014/reg014.idr

module reg014

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

transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
transpose ((x:: []) :: []) = [[x]]
transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])
transpose (x :: y :: xs) 
    = let tx = transpose [x] in 
      let ux = transpose (y :: xs) in zipWith (++) tx ux