Given a mutual fixpoint:
(fix f := ... with g := ... with h := ... for f)
I would like to bring both
h into scope. However,
for only allows me to expose one identifier. Is there any way to do that in gallina?
I see that a top-level mutual
Fixpoint actually generates two nearly identical gallina terms, only differing in the exposed identifier after
for. However, I do not have the luxury to define my mutual recursive functions at top-level.
Is there any way to do that in gallina?
Last updated: Jan 29 2023 at 05:03 UTC