Amélia

Could we just have the tiny turtles be full-on entities instead of the pseudo-blocks they are now?

HEY! THE POTATO PART IS IMPORTANT, SQUID. _I NEED A TURTLE THAT BELIEVES IN ME._

> Currently let allow record pattern matches as in let (x , y) = foo in e, and where doesn't. A first step would be to also allow these in...

I understand. Apologies, I got carried off.. won't happen again. But now that the call-out has been received, can we repurpose this issue to discuss the tagging system? I'm kinda...

> but people have deviated from that to make recent or notorious components stand out more prominently I believe this makes sense.. and it also makes some sense to have...

An approach I've used is to add `{-# OPTIONS -vtc.def.fun:10 #-}` to the file and peek at the debug buffer. This causes Agda to log each function definition it type-checks,...

For reference here's the commit that caused this: https://github.com/agda/agda/commit/ff2e43639d3c7accbe5c43ae64a05c92e6d7a3c6 and the two issues it solves: https://github.com/agda/agda/issues/5579 https://github.com/agda/agda/issues/5576

Yes I can: The regression on master is as described in the issue: basically no injectivity was happening for e.g. functions that match on `Fin n`. As part of the...

I'm not sure I like this change — the part of the documentation you're changing isn't meant to document the _literal_ primitives (that's the wall of code listings at the...

> How important is it for you to have the feature in 2.6.3 rather than just on a branch (with the prospect of entering 2.6.4)? @andreasabel I don't mind at...