[Agda] Why is refine not working right with "_,_"?

[Ulf Norell]

On Sun, May 11, 2008 at 7:06 PM, Samuel Bronson <naesten at gmail.com> wrote:

> On Sun, May 11, 2008 at 6:14 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> > If you replace the ? by {! !} I believe the emacs mode will recognize it
> as
> > a hole.
>
> Why doesn't Agda print it that way, then? I bet that would make it work...


I suppose that would be a quick work-around for the problem in this case.
The bug would still be there though.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080511/1b2f2c27/attachment.html