From 61549e3d703bdc5a017833a01febb9c46d95ec17 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 7 Jul 2026 13:09:11 -0700
Subject: Update matrices and vectors

---
 Data/Matrix/Vec.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/Data/Matrix/Vec.agda b/Data/Matrix/Vec.agda
index e0312d4..b191052 100644
--- a/Data/Matrix/Vec.agda
+++ b/Data/Matrix/Vec.agda
@@ -2,10 +2,9 @@
 
 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)
+open import Level using (Level)
 
 private
   variable
-- 
cgit v1.2.3