Nils Anders Danielsson
Nils Anders Danielsson
For consistency, wouldn't it be better to add the telescopes to all definitions in `openpublic`, whether they are defined locally or re-exported? (See #892 for a long discussion about this,...
I just think that the current feature is not very aesthetic. If I have a function `f x = record { … }`, then I do not expect to be...
Emacs complained when I tried to compile your code (`make install-bin compile-emacs-mode`): ``` In toplevel form: […]/Agda-2.9.0/emacs-mode/agda2-mode.el:2257:1:Error: the function ‘xref-apropos-regexp’ is not known to be defined. Unable to compile the...
> @nad Can you try upgrading xref from ELPA? I don't think we should require users of Agda to do that.
> Would be interesting to see whether `tog` has the same problem. @vlopezj, would you like to take a look?
I guess that you can fake "pointless" indices by adding extra constructor arguments and equality proofs.