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/FreeSemimodule.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Data/Matrix/FreeSemimodule.agda') diff --git a/Data/Matrix/FreeSemimodule.agda b/Data/Matrix/FreeSemimodule.agda index ae5822f..77f2fe3 100644 --- a/Data/Matrix/FreeSemimodule.agda +++ b/Data/Matrix/FreeSemimodule.agda @@ -13,7 +13,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Categories.Functor using (Functor) open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism) open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-[]) -open import Data.Matrix.Core R.setoid using (Matrix; module ≋; mapRows) +open import Data.Matrix.Core R.setoid using (Matrix; module ≋) open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕]) open import Data.Nat using (ℕ) open import Data.Vec using (map) -- cgit v1.2.3