From f7091746dcae0aacd0fc8c8971d6dc5a748e7bc5 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 22 Aug 2026 14:52:16 -0500
Subject: Add more matrix operations

---
 Data/Matrix/Monoid.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda
index f614dc6..719d78a 100644
--- a/Data/Matrix/Monoid.agda
+++ b/Data/Matrix/Monoid.agda
@@ -10,7 +10,7 @@ module M = Monoid M
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 
-open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _∷ᵥ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
+open import Data.Matrix.Raw as Raw using (_ᵀ; _∷ₕ_; _∷ᵥ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
 open import Data.Matrix.Core M.setoid using (Matrix; _≋_)
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec; replicate; zipWith)
@@ -28,14 +28,14 @@ private
 
 opaque
 
-  unfolding Matrix
+  unfolding Raw.Matrix
 
   𝟎 : Matrix A B
   𝟎 {A} {B} = replicate B ⟨ε⟩
 
   opaque
 
-    unfolding _ᵀ []ᵥ ⟨ε⟩
+    unfolding []ᵥ ⟨ε⟩
 
     𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B}
     𝟎ᵀ {zero} = ≡.refl
-- 
cgit v1.2.3