[Agda] Surprising type error in implementing decreasing lists

[Alan Jeffrey]

Excellent!

The bug report page suggested a work-around too, which is to define lt 
with all four cases, so it fails the injectivity checker.

A.

On 07/20/2010 05:20 AM, Ulf Norell wrote:
>
>
> On Tue, Jul 20, 2010 at 10:20 AM, Nils Anders Danielsson
> <nad at cs.nott.ac.uk <mailto: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