[Agda] FixPoint.unfold-wfRec, but for lexicographic induction?
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?
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda