Jacques Carette
Jacques Carette
> I could make your code type-check quickly by making functor= opaque. (After replacing the pattern-matching lambdas in its type with regular lambdas.) So what's the take home wrt Agda...
Let me ask another way: the use of `opaque` lets us regain some efficiency -- good. But why is this necessary at all? (Genuinely asking!) Is it somehow fundamental to...
Could you phrase your "decisions to be made" crisply? I feel like I can't give any opinion right now, as I'm not quite sure what I have to give an...
Those are quite crisp, thank you. - I do think we should have a simple interpretation of what left/right means, and be able to clearly articulate it. And that this...
I did rather expect a lot more contradictions would show up. Not sure I would be convinced by a "majority" argument unless it was > 80% on one side. Certainly...
For #2426 the main reason I'm still hesitating (even though that clearly introduce unnecessary inconsistency): what if we decide that the current handedness of the ones you changed there were...
Yep, definitely should do. Not sure when I'll get time, right now is scarily busy for me.
Yes, we can. @HuStmpHrrr if you have the time to do it, please do so. I may not get to it until late this week.
`agda-categories` still uses `--without-K` (and `safe`). We should also add `--exact-split`, but that is almost always a no-op.