Zulip Chat Archive

Stream: general

Topic: Forward declaration of meta function

Tomas Skrivan (Nov 16 2020 at 11:44):

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 (Nov 16 2020 at 11:48):

I think this should work

meta mutual def foo, bar

with foo : expr  tactic expr
| ...

with bar : expr  tactic expr
| ...

Tomas Skrivan (Nov 16 2020 at 11:49):

Thanks! I will try it out.

Reid Barton (Nov 16 2020 at 13:52):

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

Last updated: Dec 20 2023 at 11:08 UTC