Stream: MetaCoq

Topic: Shape of case branches


view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 13:13):

Is there a lemma somewhere that states that case branches are iterated lambdas?

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 13:17):

I guess this is not required by the typing relation, so I suppose it doesn't hold. But it is always true for quoted Coq terms, right?

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 19:48):

Nope, it's not true

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 19:49):

The stdlib produces branches without lambdas for example

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 19:50):

That might change in the future though. Pierre Marie P├ędrot has been working on a change of representation.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 19:51):

For now we do this externally, e.g. in CertiCoq there's a pass of the compiler that expands branches

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 21:14):

Aha, interesting. Is this due to internal AST manipulations within Coq? Or how does this arise?

view this post on Zulip Matthieu Sozeau (Jun 11 2020 at 09:02):

I mean the current typechecker accepts branches which don't start with lambdas for the arguments, and such terms are produced by the automatic schemes for example.

view this post on Zulip Jakob Botsch Nielsen (Jun 11 2020 at 09:07):

Ah, I see.


Last updated: Aug 11 2022 at 02:03 UTC