[Agda] Abusing the GADT syntax

[Ulf Norell]

On Sun, May 18, 2008 at 9:42 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw>
wrote:

> Hi,
>
>  data Acc {A : Set}(R : Rel A A) : A -> Set where
>    acc : (R ⍀ Acc R) ⊆ Acc R                             (3)


>   The constructor acc expects 0 arguments, but has been given 2
>
> Is it a bug? Or is it a bug to allow (3) in the first
> place? I would certainly prefer that Agda does allow (3). :)


It looks like a bug. I suspect the type of acc isn't being unfolded enough
at some point.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080518/001841be/attachment.html