Phantom arguments in functions [Re: [Agda] another possible without-K problem]

Nils Anders Danielsson nad at
Thu Aug 22 18:23:49 CEST 2013

On 2013-07-10 21:09, Dan Licata wrote:
> Also: does anyone know if there is a nice way to install and switch
> between multiple versions of Agda? How would I have from cabal
> and the devel version installed simultaneously?

It's easy if you don't use the Emacs mode:

   cabal install Agda
   cabal install Agda- --program-suffix=-

Then agda gives you the development version, and agda- gives you

Switching between different versions of Agda in Emacs is a bit trickier.
Two (untested) options:

* Fiddle with paths or symlinks to make sure that agda and agda-mode
   refer to the version you are interested in, and restart Emacs.

* Replace

     (load-file (let ((coding-system-for-read 'utf-8))
                     (shell-command-to-string "agda-mode locate")))

   in .emacs with

     (load-file (let ((coding-system-for-read 'utf-8))
                     (shell-command-to-string "agda-mode- locate")))

   (say), modify agda2-program-name so that it points to the right
   executable, and restart Emacs.


More information about the Agda mailing list