Syntax to define mut rec functions with termination proof

Stream: lean4

[Son Ho]

I would like to define mutually recursive functions which use termination_by and decreasing_by but I don't manage to get the syntax right. Is there an example somewhere that I can use as a reference?
(tagging @Jonathan Protzenko to keep him in the loop)

[Chris Bailey]

There are some examples in Lean's test suite, specifically this directory; check the files that start with mutwf.

[Chris Bailey]

There's also ack.lean for a classic example, but the ackermann function one is pretty simple so it might not address your use case.

[Jonathan Protzenko]

thanks Chris!

[Son Ho]

Thanks!