Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by default, it is possible to define and run programs containing general recursion. This is subject to some restrictions though:
* You can't unfold the definition to try to prove `foo = foo + 1` (which is of course false for any natural number), it is an "opaque" definition and its value for specification purposes is essentially arbitrary and does not need to match the definition.
* Even then there is a possibility of proving false things as in `partial def loop : False := loop`, so to prevent inconsistency the target type (`Nat` in the previous example, `False` in this one) must be inhabited (proved automatically by the typeclass machinery). So it would reject the `loop` example but not `foo`.
* You can't unfold the definition to try to prove `foo = foo + 1` (which is of course false for any natural number), it is an "opaque" definition and its value for specification purposes is essentially arbitrary and does not need to match the definition.
* Even then there is a possibility of proving false things as in `partial def loop : False := loop`, so to prevent inconsistency the target type (`Nat` in the previous example, `False` in this one) must be inhabited (proved automatically by the typeclass machinery). So it would reject the `loop` example but not `foo`.