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: Aug 03 2023 at 10:10 UTC