[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:



More information about the Agda mailing list