Stream: Coq users

Topic: Gallina: mutual fixpoint, multiple definitions


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaƫtan Gilbert (May 06 2021 at 17:35):

Is there any way to do that in gallina?

no :(


Last updated: Jan 29 2023 at 05:03 UTC