[Agda] on `data' syntax

Nils Anders Danielsson nad at chalmers.se
Wed Aug 22 16:34:06 CEST 2012

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:



More information about the Agda mailing list