diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b3079dee4..c690740a1e 100644 --- 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 index 4c5801fd7b..4d469a205c 100644 --- 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)