On 2012-01-09 06:03, Anthony de Almeida Lopes wrote: > In Agda, I believe it's use is invoked by prefacing a block of > data declarations by the keyword "mutual." In the latest version of Agda you can also use "forward declarations", see the release notes: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-0 -- /NAD