[Agda] Odd `with' desugaring?

[Daniel Peebles]

Hi Nils,

Sorry for the delay! I just checked the bug tracker and bug 206 already
seems to cover my case.

I'll try out your suggestion, too.

Thanks,
Dan

On Tue, Dec 22, 2009 at 5:40 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> On 2009-12-20 02:26, Daniel Peebles wrote:
>
>> This fails with:
>>
>> Dec (i' ≡ j) !=< Level of type Set
>>
>> on the i ≟ j line, supposedly in the `w' expression. I'm not really
>> sure where `w' came from so I'm assuming it's from the desugaring of
>> the with construct.
>>
>
> Right. It seems as if the auxiliary function generated by the with
> machinery does not type check. This looks like a bug. Can you open a
> ticket for it?
>
>
>  As a workaround, if I manually make a q function that takes the Dec
>> result of i ≟ j and matches on it, the whole thing works fine.
>>
>
> An easier option is perhaps to bind E in the top-level definition, so
> you don't need to quantify over it in p.
>
> --
> /NAD
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091227/c2212326/attachment.html