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