Jesper Cockx

I've added a highlights section to the top of the Changelog.

Removing the unnecessary pattern lambdas and adding `--inversion-max-depth=3`, you get: ```agda {-# OPTIONS --inversion-max-depth=3 #-} open import Agda.Builtin.List open import Agda.Builtin.Equality private variable A : Set; P : A →...

Yes, that's correct. Remembering the set of possible head symbols is something we already do I believe, the tricky thing in this case is that one of the heads is...

Yes, I think this would definitely make sense. 1 and 2 are obviously useful, while 3 would require a bit of careful design to avoid problems with subject reduction. Perhaps...

Note that the `reduce` primitive of the reflection API is just a function producing a reflected `Term` that will be typechecked when it is unquoted, (with the full set of...

Not that I know of

I think we're too close to the release now to change the language, so I have reverted the fix of #5600 (and hence made Agda treat not yet defined functions...

Since I'd like to have this in the release of Agda 2.6.3, I have hidden the option under a flag for now. Once we drop support for GHC 8.0, we...

> which can't use !editorHasSelection for obvious reasons. Why not? In Emacs this just gives the definition of the symbol at the current position of the cursor, so we could...

According to https://github.com/agda/agda/pull/6123#issuecomment-1472151296, this should only be merged AFTER #6536