Section 1.5: Datatypes and Patterns - Termination discussion

Thanks a lot for the book. I've really enjoyed working through it so far and the quality is great.

I had a couple of things that slightly confused me, maybe this is useful to clarify in the text:

Unlike many languages, Lean ensures by default that every recursive function will eventually reach a base case. From a programming perspective, this rules out accidental infinite loops.

A consequence of this is that Lean will not accept a version of even that attempts to invoke itself recursively on the original number.

It was not clear to me immediately what this means. I assumed that Lean will somehow by default refuse to run a recursive function that is not proven to terminate. I tested this (VSCode), and it crashed the Lean language process, so it appears it did just run the function. I think it would help here to clarify what the purpose is of the termination checks (eg something about the value of the diagnostics, but that it does not prevent the function from running).

Start with Section 1.5, “Datatypes and Patterns,” and review the quoted discussion of recursive termination alongside the reported VSCode behavior. Clarify what termination checks and their diagnostics mean, including whether they prevent a function from running, and verify the revised explanation in VSCode.