Forward declaration of meta function

Stream: general

[Tomas Skrivan]

Is it possible to forward declare a meta function? I have two recursive functions that call each another. I can probably merge them into one function, but conceptually it makes sense to keep them separate. I.e. I want to write code that looks something like this:

/- forward declaration -/
meta constant foo : expr -> tactic expr
meta constant bar : expr -> tactic expr

/- Actual definition of those functions -/
meta def foo : expr -> tactic expr :=  ...'implementation calling `bar`...
meta def bar : expr -> tactic expr := ...'implementation calling `foo` ...

I'm used to doing this in C++ maybe it is an incorrect way of doing things in Lean.

[Edward Ayers]

I think this should work

meta mutual def foo, bar

with foo : expr → tactic expr
| ...

with bar : expr → tactic expr
| ...

[Tomas Skrivan]

Thanks! I will try it out.

[Reid Barton]

See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/mutual.20recursion/near/213710772 if the mutual def approach seems too unwieldy