When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’

When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#The-Lean-Language-Reference--Definitions--Recursive-Definitions--Well-Founded-Recursion--Termination-proofs https://lean-lang.org/doc/reference/latest/Definitions/Recur...