fix toList-replicate's statement about vectors (#2261)

agda · Jan 20, 2024 · f59a634 · f59a634
1 parent 3515c22
commit f59a634
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -9,6 +9,10 @@ Highlights
 Bug-fixes
 ---------
 
+* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate`
+  was mistakenly applied to the level of the type `A` instead of the
+  variable `x` of type `A`.
+
 Non-backwards compatible changes
 --------------------------------
 

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
@@ -1144,7 +1144,7 @@ zipWith-replicate₂ _⊕_ (x ∷ xs) y =
   cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
 
 toList-replicate : ∀ (n : ℕ) (x : A) →
-                   toList (replicate n a) ≡ List.replicate n a
+                   toList (replicate n x) ≡ List.replicate n x
 toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)