[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