Is there a lemma somewhere that states that case branches are iterated lambdas?
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?
Nope, it's not true
The stdlib produces branches without lambdas for example
That might change in the future though. Pierre Marie Pédrot has been working on a change of representation.
For now we do this externally, e.g. in CertiCoq there's a pass of the compiler that expands branches
Aha, interesting. Is this due to internal AST manipulations within Coq? Or how does this arise?
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.
Ah, I see.
Last updated: Feb 09 2023 at 02:02 UTC