[Agda] Agda-mode and imported names

Pepijn Kokke pepijn.kokke at gmail.com
Thu Aug 21 12:05:04 CEST 2014


In agda-mode, when displaying values imported from modules with parameters,
they are displayed as, e.g.

    .#Context-110877108.[]

In addition, when using automatic rewriting, such as automatic casing (C-c
C-c) the patterns are written as such.

Is there any way to avoid this, and have agda-mode use the simple imported
name

     []

instead?

Pepijn
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140821/76338027/attachment.html


More information about the Agda mailing list