Jacques Carette
Jacques Carette
This is definitely about Agda's handling of 'irrelevant' (which I've run into quite a bit too). A discussion about it should happen on the Agda side (either Zulip or git...
Good point: I think that the proposal goes one step too far. Indeed it would only break rather strange code, but the debugging pain would be quite something!
Do we have the time to deal with this in the time remaining? Seems big! I'd want to leave this to last.
Should be careful to not say that the method can't work, just that we couldn't make it work. Understanding the 'why' could be pointed out at potential future work.
I thought it was now 'conventional wisdom' that there should be something like `let` in Agda's internal syntax, but no one has done it because it is a large job....
While I'm assigned this (and I don't mind), right now, I'm not quite sure what ought to be done. It feels like enough things have "moved underneath" that I'm not...
I could definitely warm up to this too.
It's down to working habits: I make more, smaller PRs, comprising multiple commits. You do larger chunks. If you sort by lines added, you far, far outstrip me as a...
Bumping this back up onto people's radar. 2.0 would be a good milestone to send to JOSS.
Sorry, I was unclear: of course I don't mean to go to complex numbers or any other such things. I meant to generalize `_C_` to agree (semantically) with that generalized...