From 6a35dcbbf1b3859b012e5f8546e8cb353898bde2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 2 Apr 2026 20:27:02 -0500 Subject: Reorganize matrix code --- Data/Vector/Bisemimodule.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'Data/Vector/Bisemimodule.agda') diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda index d895459..e38536a 100644 --- a/Data/Vector/Bisemimodule.agda +++ b/Data/Vector/Bisemimodule.agda @@ -136,19 +136,19 @@ opaque unfolding _∙_ ⟨ε⟩ - ∙-identityˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0# - ∙-identityˡ [] = refl - ∙-identityˡ (x ∷ V) = begin + ∙-zeroˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0# + ∙-zeroˡ [] = refl + ∙-zeroˡ (x ∷ V) = begin 0# * x + ⟨ε⟩ ∙ V  ≈⟨ +-congʳ (zeroˡ x) ⟩ - 0# + ⟨ε⟩ ∙ V  ≈⟨ +-congˡ (∙-identityˡ V) ⟩ + 0# + ⟨ε⟩ ∙ V  ≈⟨ +-congˡ (∙-zeroˡ V) ⟩ 0# + 0#  ≈⟨ +-identityˡ 0# ⟩ 0# ∎ - ∙-identityʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0# - ∙-identityʳ [] = refl - ∙-identityʳ (x ∷ V) = begin + ∙-zeroʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0# + ∙-zeroʳ [] = refl + ∙-zeroʳ (x ∷ V) = begin x * 0# + V ∙ ⟨ε⟩ ≈⟨ +-congʳ (zeroʳ x) ⟩ - 0# + V ∙ ⟨ε⟩ ≈⟨ +-congˡ (∙-identityʳ V) ⟩ + 0# + V ∙ ⟨ε⟩ ≈⟨ +-congˡ (∙-zeroʳ V) ⟩ 0# + 0# ≈⟨ +-identityˡ 0# ⟩ 0# ∎ -- cgit v1.2.3