[Agda] recursion, lexicographic ordering

[Matthew Daggitt]

Hi Jeremy,
 So I've been meaning to get rid of `Induction.WellFounded.Lexicographic`
for a while as it doesn't mesh with the rest of the library very well. Your
question might actually provide me the impetus to do so!

Give me a few hours to upload a new branch to the standard library with
some small changes and I'll get back to you with the best way to do so.
Best,
Matthew


On Sat, Feb 29, 2020 at 1:05 PM Siek, Jeremy <jsiek at indiana.edu> wrote:

> I would like to define a function (Martello and Montanari’s unification
> algorithm)
> whose termination measure is a lexicographic ordering of three numbers.
> I get the impression that there is support for this kind of thing in the
> standard library, in Induction.WellFounded.Lexicographic.
> However, I’m at a loss trying to figure out how to use it.
> Any examples or pointers to documentation or tutorials
> would be much appreciated.
>
> Thank you,
> Jeremy
>
>
>
>
>
> _______________________________________________
> 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/20200229/a5fa105a/attachment.html>