diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
| commit | f7091746dcae0aacd0fc8c8971d6dc5a748e7bc5 (patch) | |
| tree | 9966acfbd9584af65d1f20f99e051bdc94ecd63b /Data/Matrix/Monoid.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/Monoid.agda')
| -rw-r--r-- | Data/Matrix/Monoid.agda | 6 |
1 files changed, 3 insertions, 3 deletions
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 |