Move location of take-[] and drop-[] in CHANGELOG.md (#1991)

agda · Oct 13, 2023 · 4b008d6 · 4b008d6
1 parent b4fa218
commit 4b008d6
Showing 1 changed file with 3 additions and 6 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -2082,6 +2082,9 @@ Other minor changes
 
  length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
  length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
+ 
+ take-[] : ∀ m → take m [] ≡ []
+ drop-[] : ∀ m → drop m [] ≡ []
  ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2813,12 +2816,6 @@ Other minor changes
  foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
  foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
  ```
-
- * Added new lemmas in `Data.List.Propreties`:
- ```
- take-[] : ∀ m → take m [] ≡ []
- drop-[] : ∀ m → drop m [] ≡ []
- ```
 
 NonZero/Positive/Negative changes
 ---------------------------------