File tree 1 file changed +4
-4
lines changed
1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -2165,9 +2165,9 @@ Other minor changes
2165
2165
take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
2166
2166
drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ]
2167
2167
drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ]
2168
-
2169
- take-all : n ≥ length xs → take n xs ≡ xs
2170
-
2168
+
2169
+ take-all : n ≥ length xs → take n xs ≡ xs
2170
+
2171
2171
take-[] : ∀ m → take m [] ≡ []
2172
2172
drop-[] : ∀ m → drop m [] ≡ []
2173
2173
```
@@ -2901,7 +2901,7 @@ Other minor changes
2901
2901
foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
2902
2902
foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
2903
2903
```
2904
-
2904
+
2905
2905
NonZero/Positive/Negative changes
2906
2906
---------------------------------
2907
2907
You can’t perform that action at this time.
0 commit comments