Forward and backwards recursion

Stream: general

[Zahir Bingen]

Hello everyone,
I have a simple question about LEAN3. All the recursive functions I have made are recursing backwards. Is this actually a requirement, to guarantee termination of the function? Or is it also possible to do forwards recursion with a proof that the function will terminate?

[Trebor Huang]

Forwards recursion is also possible. See termination_by for providing termination proofs in this case.