[Agda] FixPoint.unfold-wfRec, but for lexicographic induction?

Siek, Jeremy jsiek at indiana.edu
Fri Jun 3 02:08:04 CEST 2022

The answer to my question is to use the lexicographic induction from
which is formulated as an instance of well founded induction, and then
I can use the same unfold-wfRec.

I had been using the lexicographic induction from 
but it seems that this was a red herring.


> On Jun 2, 2022, at 3:50 PM, Siek, Jeremy <jsiek at indiana.edu> wrote:
> Hi all,
> When reasoning about recursive functions defined using the WellFounded library, the FixPoint.unfold-wfRec lemma is very useful. However, now I find myself needing to do lexicographic induction over two well-founded inductions. Is there an equivalent of unfold-wfRec that works for lexicographic induction?
> Cheers,
> Jeremy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

More information about the Agda mailing list