[Agda] on `data' syntax

[Nils Anders Danielsson]

On 2012-08-21 20:54, Serge D. Mechveliani wrote:
> definition 1  is compiled,
> and  definition 2   is not compiled:
>                      "p not in scope"  in the line of  `intRes ...'

Index variables are not in scope in the constructor types:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Data

-- 
/NAD