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/Cast.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/Cast.agda')
| -rw-r--r-- | Data/Matrix/Cast.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Data/Matrix/Cast.agda b/Data/Matrix/Cast.agda index 43c50c8..a0fa92f 100644 --- a/Data/Matrix/Cast.agda +++ b/Data/Matrix/Cast.agda @@ -7,7 +7,7 @@ module Data.Matrix.Cast {c ℓ : Level} (S : Setoid c ℓ) where module S = Setoid S -open import Data.Matrix.Raw using (_∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ) +open import Data.Matrix.Raw as Raw using (_∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ) open import Data.Matrix.Core S using (Matrix; _≋_) open import Data.Nat using (ℕ; _+_) open import Data.Nat.Properties using (suc-injective; +-assoc) @@ -25,7 +25,7 @@ private opaque - unfolding Matrix + unfolding Raw.Matrix cast₁ : .(A ≡ B) → Matrix A C → Matrix B C cast₁ eq = map (castVec eq) |