blob: e0312d492985c68fe04ba48ccfeb75fba969f0d0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
{-# OPTIONS --without-K --safe #-}
module Data.Matrix.Vec where
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Level using (Level)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; replicate; zipWith)
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)
|
