Are all recursive functions implemented with .brecOn?

Stream: lean4

[nrs]

Given a recursive function where each step contains actual data, is such a function always implemented through .brecOn? Otherwise, when are dataful recursive functions, i.e., recursive functions where there is data being manipulated at each step, implemented with .brecOn, and what is used to implement dataful functions in other cases?

[Mario Carneiro]

Lean has two equation compilation (or "derecursification") strategies: bounded structural recursion, and well founded recursion. The former is used by most regular functions, while the latter typically involves using termination_by and decreasing_by (although lean makes its best guess at these if you don't specify). Bounded structural recursive definitions will have T.brecOn in the #print result, and well founded recursive definitions will have WellFounded.fix (hidden behind a myfunc._unary auxiliary).

[Mario Carneiro]

Primitive structural recursion is actually not supported by lean, so you will not be able to get it to output definitions using T.recOn using the equation compiler

[nrs]

I see! Thanks a lot for taking the time, I couldn't find this anywhere but was seeing a glimpse of this in #print results without understanding why