spaceloop (May 06 2021 at 17:28): spaceloop (May 06 2021 at 17:28):Given a mutual fixpoint:
(fix f := ...
with g := ...
with h := ...
for f)
I would like to bring both f, g and h into scope. However,for only allows me to expose one identifier. Is there any way to do that in gallina?
spaceloop (May 06 2021 at 17:35):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.
Gaëtan Gilbert (May 06 2021 at 17:35):Is there any way to do that in gallina?
no :(
Last updated: Apr 19 2024 at 12:02 UTC