Stream: Coq devs & plugin devs

Topic: CaseInvert w.r.t. case change of repr


view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:04):

@Gaëtan Gilbert I'll need your help for the rebase of my branch, since there are invariants I am not quite sure about.

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:04):

More generally, the typing rules of CaseInvert ought to be better stated.

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 19:13):

in your branch you have Case of univs * params * ...
when CaseInvert you also need the indices

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:14):

Right, but what about the let-bindings of the arity?

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:15):

The system also enforces that the body has no binder at all, right?

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:15):

Or does it have let bindings potentially?

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 19:23):

I have no clue what you're talking about
what do let bindings have to do with caseinvert?

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:24):

You can have let-bindings in the arity and in the unique branch for the constructor.

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:24):

I need to understand a bit what are the invariants and the exact context in which the subterms live.

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 19:24):

right now I have to go, but we can talk later / tomorrow.


Last updated: Oct 21 2021 at 21:03 UTC