[Agda] recursion, lexicographic ordering

[Siek, Jeremy]

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





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200229/f3bfde4b/attachment.html>