Docs for how to prove termination of recursive function?

Stream: new members

[aron]

I haven't been able to find any documentation for how to prove that a recursive function terminates when Lean can't figure it out automatically. Are there any docs for this?
I don't even know how it works syntactically. Does the termination_by clause go in a specific place or can it go anywhere in the function body?

[Ruben Van de Velde]

It goes after the function body

[Markus Himmel]

You can have a look at the reference manual, which contains some examples.

[Ruben Van de Velde]

And if that doesn't help, you can search in mathlib

[Joachim Breitner]

https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/ is also worth looking at