Ensuring tail recursion

Stream: lean4

[Siddhartha Gadgil]

In scala, I can annote a method as @annotation.tailrec def ... so that it is a compiler error if the method cannot be tail call optimized. I was wondering if there is something like this in lean 4. I do know when a method is supposed to be tail recursive but judging by eye is a little fiddly.

[Sebastian Ullrich]

That would be nice, though we cannot guarantee mutual TCO yet anyway https://github.com/leanprover/lean4/pull/606#issue-704444706