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/Core.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/Core.agda')
| -rw-r--r-- | Data/Matrix/Core.agda | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Data/Matrix/Core.agda b/Data/Matrix/Core.agda index 4ef57fb..fef4274 100644 --- a/Data/Matrix/Core.agda +++ b/Data/Matrix/Core.agda @@ -31,7 +31,8 @@ private module PW-≊ {n} = PW-≈ (Vectorₛ n) -open Raw.FixedBase Carrier using (Matrix) public +Matrix : ℕ → ℕ → Set c +Matrix = Raw.Matrix Carrier opaque |