[Agda] bug in definitions using "_"?

Jesper Cockx Jesper at sikanda.be
Thu Dec 19 17:17:17 CET 2013


This is indeed fixed in the development version: see
http://code.google.com/p/agda/issues/detail?id=920.

Jesper


On Thu, Dec 19, 2013 at 12:00 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

>
>
> On 19/12/13 10:37, Ulf Norell wrote:
>
>> It looks like this has been fixed. In the development version I get
>> yellow on all variants of the example.
>>
>
> Great. Fortunately I don't use "_" often in proofs. But I worry that
> the one or two occasions in which I did may be unfillable!
>
> I shall try the development version.
>
> Thanks,
>
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131219/872f0dcc/attachment.html


More information about the Agda mailing list