Nils Anders Danielsson

The following code triggers an internal error: ```agda {-# OPTIONS --type-based-termination #-} open import Agda.Primitive postulate A : Set a : A P : (A : Set) → A →...

Here is another problem: ```agda {-# OPTIONS --type-based-termination --no-syntax-based-termination #-} postulate P : (A : Set) → A → Set f : (A : Set) (x : A) → P...

Here is another problem: ```agda {-# OPTIONS --type-based-termination #-} data F (A : Set) : Set where c₁ : A → F A f : (A B : Set) →...

Perhaps one can track down the problem by using `agda-bisect` with the `--timeout` flag.

It seems as if you have not installed the [`timeout`](https://www.gnu.org/software/coreutils/manual/html_node/timeout-invocation.html) command. I recommend that you use `--dry-run` before starting the bisection process.

I have not read the entire discussion, but I want all features that introduce "lossiness" to be off by default, and turned on by infective flags (so that one cannot...

Note that the Agda input method (by default) inherits some key bindings from Emacs' TeX input method: https://github.com/agda/agda/blob/fbf9d159c3c874b8328ccdc78a0d57d57a310234/src/data/emacs-mode/agda-input.el#L150-L175 If you dump those key bindings to a file and use them...

This pull request seems to be incompatible with pull request #6538.

> The functionality is currently rather rudimentary and will only consider loaded buffers. This might lead to some false-positives, but I haven't noticed any while playing around with the Agda...

> Correct that to _comment-out dead code_. I don't quite agree with you here. If you want to document some design decision, preserving lots of commented-out source code is not...