well foundness in the kernel

Stream: general

[Paul-Nicolas Madelaine]

Hi everyone,

I'm running in some issues with well foundness. I defined a function using the using_well_founded key word and a well founded relation that I defined.
My function is running fine in the VM, but it seems like the kernel is not computing the function at all, for instance when I'm applying reflexivity.
I don't even get a timeout, the elaborator just fails immediatly.

Did anyone encountered similar issues with well foundness blocking computation in the kernel?

[Wojciech Nawrocki]

Yep, I just ran into this - see Mario's answer in ( https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/170801612 ). The kernel will properly reduce structurally recursive calls, but not ones using well_founded.fix.