Zulip Chat Archive

Stream: general

Topic: well foundness in the kernel


Paul-Nicolas Madelaine (Jul 18 2019 at 12:52):

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 (Jul 18 2019 at 15:16):

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.


Last updated: Dec 20 2023 at 11:08 UTC