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

Samuel Bronson naesten at gmail.com
Sun May 11 19:06:10 CEST 2008


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...


More information about the Agda mailing list