blob: b191052615ad0a3a5ce65b4129d59258c8b7678a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# OPTIONS --without-K --safe #-}
module Data.Matrix.Vec where
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; replicate; zipWith)
open import Level using (Level)
private
variable
a : Level
A : Set a
n m : ℕ
open Vec
transpose : Vec (Vec A n) m → Vec (Vec A m) n
transpose [] = replicate _ []
transpose (row ∷ mat) = zipWith _∷_ row (transpose mat)
|
