From 6a35dcbbf1b3859b012e5f8546e8cb353898bde2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 2 Apr 2026 20:27:02 -0500
Subject: Reorganize matrix code

---
 Data/Matrix/Vec.agda | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Data/Matrix/Vec.agda

(limited to 'Data/Matrix/Vec.agda')

diff --git a/Data/Matrix/Vec.agda b/Data/Matrix/Vec.agda
new file mode 100644
index 0000000..e0312d4
--- /dev/null
+++ b/Data/Matrix/Vec.agda
@@ -0,0 +1,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)
-- 
cgit v1.2.3