diff options
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 |