diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-07 13:09:11 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-07 13:09:11 -0700 |
| commit | 61549e3d703bdc5a017833a01febb9c46d95ec17 (patch) | |
| tree | 7b3aabbe8ddb5d2316cb24368edde212e27d8c1a /Data/Vector/Monoid.agda | |
| parent | be685059304423e5a5cbb176b44aef1a4a76325b (diff) | |
Update matrices and vectors
Diffstat (limited to 'Data/Vector/Monoid.agda')
| -rw-r--r-- | Data/Vector/Monoid.agda | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda index 5906bf9..da09de9 100644 --- a/Data/Vector/Monoid.agda +++ b/Data/Vector/Monoid.agda @@ -24,8 +24,6 @@ private opaque - unfolding Vector - -- Sum the elements of a vector sum : Vector n → M.Carrier sum = foldr′ _∙_ ε @@ -36,8 +34,6 @@ opaque opaque - unfolding Vector - -- Pointwise sum of two vectors _⊕_ : Vector n → Vector n → Vector n _⊕_ = zipWith _∙_ @@ -54,8 +50,6 @@ infixl 6 _⊕_ opaque - unfolding Vector - -- The identity vector ⟨ε⟩ : Vector n ⟨ε⟩ {n} = replicate n ε @@ -119,7 +113,7 @@ open ≡-Reasoning opaque - unfolding pull _⊕_ + unfolding _⊕_ pull-⊕ : {f : Fin A → Fin B} (V W : Vector B) → pull f ⟨$⟩ (V ⊕ W) ≡ (pull f ⟨$⟩ V) ⊕ (pull f ⟨$⟩ W) pull-⊕ {A} {B} {f} V W = begin @@ -132,7 +126,7 @@ opaque opaque - unfolding pull ⟨ε⟩ + unfolding ⟨ε⟩ pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩ pull-⟨ε⟩ {f = f} = begin @@ -157,7 +151,7 @@ opaque {g : Fin C → Fin B} {v : Vector A} → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v) - pullₘ-∘ = S.pull-∘ + pullₘ-∘ {f = f} {g} {v} = S.pull-∘ {f = f} {g} {v} pullₘ-cong : {f g : Fin B → Fin A} |