well founded recursion is an axiom right?

Stream: general

[Huỳnh Trần Khanh]

hmm maybe I should stop posting in the new members stream because I'm not new anymore :smile: is well founded recursion an axiom or can it be expressed through structural induction/recursion?

[Mario Carneiro]

You can use #print to see what happens to definitions by well founded recursion yourself. There are no new axioms, it all comes down to the recursion principle for the carefully constructed inductive type docs#acc

[Gihan Marasingha]

It's all in the function well_founded.fix. That fix creates a function with the desired property is the lemma well_founded.fix_eq. Explaining this will be my next blog post on the topic.