> I get test "hi" reducing to true as expected. Did you get the latest Agda > version from darcs? It might be that it's an old bug that has already been > fixed. Pulling the latest patches solved the problem for me. Thanks. Cheers, Andres -- Andres Loeh, Universiteit Utrecht mailto:andres at cs.uu.nl mailto:mail at andres-loeh.de http://www.andres-loeh.de