Jakob Botsch Nielsen (Jun 10 2020 at 13:13): Jakob Botsch Nielsen (Jun 10 2020 at 13:13):Is there a lemma somewhere that states that case branches are iterated lambdas?
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?
Matthieu Sozeau (Jun 10 2020 at 19:48):Nope, it's not true
Matthieu Sozeau (Jun 10 2020 at 19:49):The stdlib produces branches without lambdas for example
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.
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
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?
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.
Jakob Botsch Nielsen (Jun 11 2020 at 09:07):Ah, I see.
Last updated: Sep 15 2024 at 13:02 UTC