Skip to content

Commit b6a31fc

Browse files
committed
fix toList-replicate's statement about vectors
1 parent 3515c22 commit b6a31fc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/Vec/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1144,7 +1144,7 @@ zipWith-replicate₂ _⊕_ (x ∷ xs) y =
11441144
cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
11451145

11461146
toList-replicate : (n : ℕ) (x : A)
1147-
toList (replicate n a) ≡ List.replicate n a
1147+
toList (replicate n x) ≡ List.replicate n x
11481148
toList-replicate zero x = refl
11491149
toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
11501150

0 commit comments

Comments
 (0)