Nils Anders Danielsson

> We typically read these first-to-last but often need to append a new elimination at the end. How are these lists used? Would a FIFO queue data structure suffice, or...

> (Removing label "bug": There is no evidence for such claim here.) Here is one example. Compare Agda's performance for the following families of files: ```agda {-# FOREIGN GHC {-#...

Try with hundreds or thousands of lines instead of `⋮`.

I don't think this is very important, but Andreas asked for evidence of quadratic behaviour. Here is a possibly more relevant example of superlinear performance: ```agda postulate F : Set₁...

With the current (disabled) implementation one can get bogus links. I re-enabled the generation of links to symbolic identifiers by renaming `_aName` to `aName` and replacing line 428 with line...

If this issue is fixed, then I suggest that we also add the HTML backend option `--html-link-to-comments`. If this option is used, then links to definitions with symbolic identifiers should...

I think you should be very careful about starting to use new top-level module names like `Equality`, at least until issue https://github.com/agda/agda/issues/4029 has been fixed. I have another library with...

I don't think any of the main Agda developers plan to fix issue https://github.com/agda/agda/issues/4029 any time soon. However, once we have settled on a design I think it would be...

It seems to me as if it would not make sense to make the generated `transpX` constructors erased. Does it still make sense to erase them, and the generated clauses,...

> The flag `-vtc.def.fun.clauses:15` can be used to print out the final clauses for a function definition. And the flag ` -vtc.transpix.type:15` can be used to print out the type...