diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-09 10:24:03 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-09 10:24:03 -0700 |
| commit | 50b9117ebac5f16db7b2ddc59c52a28129e0a618 (patch) | |
| tree | cce919ee920a9ac9f0f93efb05260c87338c8ae2 /Data/Matrix/Functional.agda | |
| parent | 6a0549f4c5a93a1817cd311440de156c3283ba27 (diff) | |
Include missing properties
Diffstat (limited to 'Data/Matrix/Functional.agda')
| -rw-r--r-- | Data/Matrix/Functional.agda | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Data/Matrix/Functional.agda b/Data/Matrix/Functional.agda index 2f9a85d..bbfd53c 100644 --- a/Data/Matrix/Functional.agda +++ b/Data/Matrix/Functional.agda @@ -10,6 +10,7 @@ open import Data.Fin using (Fin; _≟_) open import Data.Nat using (ℕ) open import Data.Vec.Functional using (Vector; head; tail) open import Function using (flip) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) open import Relation.Nullary.Decidable using (⌊_⌋) open Semiring R @@ -22,6 +23,10 @@ sum : {n : ℕ} → Vector Carrier n → Carrier sum {zero} _ = 0# sum {suc n} v = head v + sum (tail v) +sum-cong : {n : ℕ} {V W : Vector Carrier n} → V ≗ W → sum V ≡ sum W +sum-cong {zero} V≗W = ≡.refl +sum-cong {suc n} {V} {W} V≗W = ≡.cong₂ _+_ (V≗W Fin.zero) (sum-cong (λ i → V≗W (Fin.suc i))) + _⟨*⟩_ : {n : ℕ} → Vector Carrier n → Vector Carrier n → Vector Carrier n _⟨*⟩_ v w i = v i * w i |