[Agda] Agda-mode and imported names

[Pepijn Kokke]

Yes, it seems to be this issue. Thanks for the link! :)


On 21 August 2014 13:38, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140821/2e3c6eef/attachment.html