[Agda] Agda-mode and imported names

[Andrea Vezzosi]

Hi,

Does it happen only for constructors? If so it seems to be this bug:

https://code.google.com/p/agda/issues/detail?id=896

Cheers,
Andrea


On Thu, Aug 21, 2014 at 12:05 PM, Pepijn Kokke <pepijn.kokke at gmail.com> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>