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/Vector | |
| parent | 6a0549f4c5a93a1817cd311440de156c3283ba27 (diff) | |
Include missing properties
Diffstat (limited to 'Data/Vector')
| -rw-r--r-- | Data/Vector/Vec.agda | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda index 4367bdd..74ab0cc 100644 --- a/Data/Vector/Vec.agda +++ b/Data/Vector/Vec.agda @@ -27,8 +27,9 @@ private zipWith-tabulate : {n : ℕ} - (_⊕_ : A → A → A) - (f g : Fin n → A) + (_⊕_ : A → B → C) + (f : Fin n → A) + (g : Fin n → B) → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i) zipWith-tabulate {n = zero} _⊕_ f g = ≡.refl zipWith-tabulate {n = suc n} _⊕_ f g = ≡.cong (f zero ⊕ g zero ∷_) (zipWith-tabulate _⊕_ (f ∘ suc) (g ∘ suc)) |