Skip to content

Commit 4e16643

Browse files
authored
[ fix #1338 ] Made Data.Vec._⊛_ stricter (#1342)
1 parent 77c31ff commit 4e16643

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/Vec/Base.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ _⋎_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
149149
infixl 4 _⊛_
150150

151151
_⊛_ : {n} Vec (A B) n Vec A n Vec B n
152-
[] ⊛ _ = []
152+
[] ⊛ [] = []
153153
(f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)
154154

155155
-- Multiplication

0 commit comments

Comments
 (0)