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

[Ulf Norell]

On Sat, May 10, 2008 at 11:44 PM, Samuel Bronson <naesten at gmail.com> wrote:

> For instance, if I start with:
>
> ×-≃ (≃-≈ xy)    (≃-≈ xy')   = ≃-≈ ({!_,_ !})
>
> and type C-c C-r, I get:
>
> ×-≃ (≃-≈ xy)    (≃-≈ xy')   = ≃-≈ ({? , {! !})
>
> where the question mark is not picked up by the emacs mode as a hole
> to put more code in...


That's a known bug:

http://code.google.com/p/agda/issues/detail?id=15

If you replace the ? by {! !} I believe the emacs mode will recognize it as
a hole.

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