jamesmckinna
jamesmckinna
Well, we now (PR #1668) have some more systematic `≡`-based `fold*-fusion` results in `Data.Vec.Properties` (and soon, some more heterogeneous ones about `reverse` to go... somewhere), so part of that reconsideration...
And my last bit of (2022!) bikeshedding on this point: I had introduced `foldr₀`, `foldl₀` for the non-dependent forms of the `Vec` folds, ignorant of the consensus here. I still...
Hmmm. Let me know how you get on with implicit `{B = ...}` in `Data.Vec`... where the library writer has lots of work to do to supply such `B`s (even...
Suggest `map-∘` throughout?
And similarly [sum-++-commute](https://agda.github.io/agda-stdlib/Data.List.Properties.html#20000). I'll open a PR.
What about the `*-commute` properties in `Data.Sum.Properties`?
@JacquesCarette I take your point about 'small' PRs: but #626 and #509 are about consistency/uniformity of names *according to a systematic library convention* (whose stipulation to a large extent is...
Thanks for clarification. Given our discussion on Monday about the 2.0 milestone, I was indeed keen to achieve 'completeness' in closing these two issues. But yes, experience with git(hub) has...
Updated `CHANGELOG`.
Outstanding instances of `-commute`: - [x] `Data.Sum.Properties` affecting `Data.Fin.Properties` and `Data.Vec.Properties` through `[,]-map-commute` and `[,]-∘-distr` (!), plus a couple of other `map-commute`-like lemmas not used elsewhere - [x] `Data.Vec.Recursive.Properties` with...