From 61549e3d703bdc5a017833a01febb9c46d95ec17 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 7 Jul 2026 13:09:11 -0700 Subject: Update matrices and vectors --- Data/Matrix/Monoid.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'Data/Matrix/Monoid.agda') diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda index b7638f6..93b449f 100644 --- a/Data/Matrix/Monoid.agda +++ b/Data/Matrix/Monoid.agda @@ -10,7 +10,8 @@ module M = Monoid M import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Data.Vec.Relation.Binary.Pointwise.Inductive as PW -open import Data.Matrix.Core M.setoid using (Matrix; _≋_; _ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) +open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥) +open import Data.Matrix.Core M.setoid using (Matrix; _≋_) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; replicate; zipWith) open import Data.Vec.Properties using (zipWith-replicate) @@ -72,7 +73,7 @@ opaque opaque - unfolding Matrix + unfolding _≋_ _[+]_ : Matrix A B → Matrix A B → Matrix A B _[+]_ = zipWith _⊕_ -- cgit v1.2.3