[Agda] Datatype parameters and indices

[Jan Malakhovski]

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,
  Jan