From 50b9117ebac5f16db7b2ddc59c52a28129e0a618 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 9 Jul 2026 10:24:03 -0700
Subject: Include missing properties

---
 Data/Vector/Vec.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Data/Vector/Vec.agda')

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))
-- 
cgit v1.2.3