Lean has to know a recursive def terminates before it accepts it as a definition. Structural recursion is found automatically…
