Jacques Carette
Jacques Carette
The various refactors nicely show the 'worth' of these changes. No strong feeling regarding 2.0/2.1.
I'm also in favour of separate sub-modules. And I, of course, have my own implementation, which is again different. See `Bag.agda` for the proof, and `SetoidPermutation.agda` for the relation, based...
I develop it all *twice*, once the CS way, and once the Math way. The Math way, when spelled out in full, is quite silly - and thus its name...
And as I said on #2284 , I think that's a reasonable suggestion. (I'm still torn because my math background wants me to see `Σ` as a sum, and I...
Yes, other than that, this looks really good!
Just need @gallais to re-review.
So I think that the stuff in #2269 doesn't really need to move? At least, I don't immediately see the need. So that leaves just `scanr`? Or do `tails` and...
That version of `scanr` would be a massive pain to prove anything about. Not only does it use a non-public helper function (whose properties are crucial), it also uses `with`...
I'm a huge believer in "follow the elegant path". Not always (there's lots of room for solid engineering and usability to disrupt some elegant paths), but whenever realistic. I sometimes...
It doesn't look like #2071 closes this, it 'only' provides the underlying machinery to get there. It feels like this new machinery should get actively used in combinators to make...