[Agda] Surprising type error in implementing decreasing lists

[Ulf Norell]

On Tue, Jul 20, 2010 at 10:20 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> On 2010-07-20 09:05, Conor McBride wrote:
>
>> If I were a betting man, I'd bet Agda is making some attempt to
>> guess which functions are injective, in order to invert them, and
>> has somehow guessed wrongly about the nature of _lt_.
>>
>
> Indeed this seems to be the case. For some reason Agda believes that
> _lt_ is "constructor-headed"
>

Fixed now. Recursive calls where mistakenly treated as constructors when
checking invertibility. All the examples from issue 246 now go through
properly.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100720/a172c316/attachment.html