@Gaëtan Gilbert I'll need your help for the rebase of my branch, since there are invariants I am not quite sure about.
More generally, the typing rules of CaseInvert ought to be better stated.
in your branch you have Case of univs * params * ...
when CaseInvert you also need the indices
Right, but what about the let-bindings of the arity?
The system also enforces that the body has no binder at all, right?
Or does it have let bindings potentially?
I have no clue what you're talking about
what do let bindings have to do with caseinvert?
You can have let-bindings in the arity and in the unique branch for the constructor.
I need to understand a bit what are the invariants and the exact context in which the subterms live.
right now I have to go, but we can talk later / tomorrow.
Last updated: Oct 21 2021 at 21:03 UTC