[Agda] Datatype parameters and indices

Jan Malakhovski oxij at oxij.org
Mon Jan 28 06:23:19 CET 2013

On Sun, 27 Jan 2013 00:32:46 +0100
Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> To spread the results of the discussion, could you imagine to summarize 
> it and integrate it into the Wiki page?
>    http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Data
> This would be greatly appreciated!!

Actually, I asked this question exactly because I'm trying to write a document (tutorial or something like) that lists and explains these subtle things in Agda and ITT that I've stumbled upon and find interesting.

I'll consider porting appropriate parts to the Reference Manual.

Best regards,

More information about the Agda mailing list