Jacques Carette
Jacques Carette
It would. Should we have a list somewhere? I will likely have summer students again. And this is much more well-delimited than some of the other things I've tried to...
This code development was indeed done "outside stdlib" while prototyping stuff to go into stdlib, and thus the warning had not been shut off. While I disagree with @plt-amy about...
Arguably, it was the original change that was `breaking` but only mildly (new warnings). So this could be seen as a bug fix.
[Recent work on Agda performance](https://github.com/agda/agda/issues/8080#issuecomment-3236745038) provides quite a bit more ammunition for doing this. `stdlib` uses `IndexedMatch` *a lot* (3926 times apparently). It's a perfectly fine feature but incompatible with...
BTW, this is not really `breaking`. This is gaining back some efficiency that we lost without sufficient discussion. One could consider this a bug fix.
Yes, there is quite a lot that can be done in this vein. We should be careful not to have perfect be the enemy of definite-improvement...
I guess, strictly speaking, neither you nor @Taneb are blocking this on requiring more features...
That's why it's Draft, I need to do at least those changes.
I guess we could back-patch v2.0 with this fix? I'm not entirely sure what the best path forward is, which is why I am keeping this commentary as a separate...
We could backpatch to the v2.0-joss-submission branch? Is v2.1 different enough from v2.0 that we can't make this paper about that? I know it is mainly about the jump from...