Jacques Carette
Jacques Carette
Agreed, i.e. I can commit to that.
Suggestions: `isYes?` and `isNo?` (i.e. with the `?`) `yes?` and `no?` . There might be other 'signs' of decidability also used in the library? I'm not entirely against `decYes` and...
I'm torn. Now that I've seen that there really ought to be two functions here, not just one, it's kind of hard to go with `dec⇒maybe`. Which speaks in favour...
First thought: what's the precedence for all of these things?
You're legitimately confused because I wrote down the wrong word! Stupid fingers. I mean 'precedence' not 'precedent' !!! (Fixed now) It was meant to be a purely technical suggestion to...
Now I've caught up with all of this, and I agree that ```agda syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs
It is a 'tiny' breaking change that shouldn't affect many people as long as they look at warnings. Do we really have to wait until v3.0 for this?
I'll whine that the Agda devs break things in this way all the time in releases (2.6.3 and 2.6.5 are not compatible because `Reflection` changed), so holding the moral high...
> In v3.0 I'd advocate removing everything deprecated in versions v1.X. So I could go ahead and do that as part of this PR?