[Agda] Termination checking with Lexicographic recursive calls

[Matthew Daggitt]

>
> Perhaps we are using different versions of the standard library. I'm
> using the branch called "experimental".
>

Looking at the code, I can't see why it shouldn't work on experimental?
What's the error you're getting Nils?

On Wed, Feb 19, 2020 at 6:58 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2020-02-18 13:27, Sergey Goncharov wrote:
> > Why do you say that the example is not self-contained? It uses the
> > standard library -- otherwise it is complete.
>
> Perhaps we are using different versions of the standard library. I'm
> using the branch called "experimental".
>
> --
> /NAD
> _______________________________________________
> 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/20200219/54828ffd/attachment.html>