Skip to content

Commit 91468bc

Browse files
authored
Move location of take-[] and drop-[] in CHANGELOG.md (#1991)
1 parent 0dd231d commit 91468bc

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

CHANGELOG.md

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2082,6 +2082,9 @@ Other minor changes
20822082
20832083
length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
20842084
length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
2085+
2086+
take-[] : ∀ m → take m [] ≡ []
2087+
drop-[] : ∀ m → drop m [] ≡ []
20852088
```
20862089

20872090
* Added new patterns and definitions to `Data.Nat.Base`:
@@ -2813,12 +2816,6 @@ Other minor changes
28132816
foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
28142817
foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
28152818
```
2816-
2817-
* Added new lemmas in `Data.List.Propreties`:
2818-
```
2819-
take-[] : ∀ m → take m [] ≡ []
2820-
drop-[] : ∀ m → drop m [] ≡ []
2821-
```
28222819

28232820
NonZero/Positive/Negative changes
28242821
---------------------------------

0 commit comments

Comments
 (0)