Amélia
> OTOH, I doubt many things (at least in the CC ecosystem) would break from lack of 5.1 bytecode support. I know potatOS uses precompiled bytecode (which is also encrypted/obfuscated),...
My two cents are worth less than y'all's due to exchange rate but I'd rather just bite the bullet and kill all the 5.1 stuff now—It's been deprecated for _years_,...
I'll keep working on it over the next week but sadly I'm not sure boundary-sensitive evaluation will be ready for review, let alone merge-able, in the coming 9 days. Bumping...
Actually, do we still need this after #6153? I don't think so
Gonna close this as superceded by the nat and ring solvers
Bumping to 2.6.4; Since #6153 this doesn't panic anymore.
Re. the TODO items: > Updating the CHANGELOG. We would appreciate some pointers as to what to write. My two cents: Something like "Introduced explicit polarity annotations (user guide link),...
Right, I'm okay with having all matching on non-`@mixed` forbidden for now. The reason I thought the above code would (should) be disallowed is that it desugars to something like...
> [_*déjà vu*_](https://lists.chalmers.se/pipermail/agda/2016/008657.html) I don't think this reaction is appropriate; it's not April. This issue is a legitimate feature request, with prior art in other proof assistants *and*, more importantly,...