aboutsummaryrefslogtreecommitdiff
path: root/Data/Vector/Bisemimodule.agda
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-07-07 13:09:11 -0700
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-07-07 13:09:11 -0700
commit61549e3d703bdc5a017833a01febb9c46d95ec17 (patch)
tree7b3aabbe8ddb5d2316cb24368edde212e27d8c1a /Data/Vector/Bisemimodule.agda
parentbe685059304423e5a5cbb176b44aef1a4a76325b (diff)
Update matrices and vectors
Diffstat (limited to 'Data/Vector/Bisemimodule.agda')
-rw-r--r--Data/Vector/Bisemimodule.agda2
1 files changed, 0 insertions, 2 deletions
diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda
index e38536a..4121b91 100644
--- a/Data/Vector/Bisemimodule.agda
+++ b/Data/Vector/Bisemimodule.agda
@@ -32,8 +32,6 @@ private
opaque
- unfolding Vector
-
-- Scaling a vector from the left
_⟨_⟩ : Carrier → Vector n → Vector n
_⟨_⟩ r = map (r *_)