[Agda] induction-recursion

Nils Anders Danielsson nad at chalmers.se
Mon Jan 9 12:06:58 CET 2012


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


More information about the Agda mailing list