Pierre-Marie Pédrot (Feb 05 2022 at 18:00): Pierre-Marie Pédrot (Feb 05 2022 at 18:00):I was pondering recently about the mismatch between the internal representation of Case nodes and what we display to the user. Since the change of representation, the gap is much narrower, but there are still differences.
Pierre-Marie Pédrot (Feb 05 2022 at 18:00):The only real difference is that we do not display parameters / universe instances of the return clause to the user.
Pierre-Marie Pédrot (Feb 05 2022 at 18:01):In practice, we force syntactically parameters of the return clause to always be underscores.
Pierre-Marie Pédrot (Feb 05 2022 at 18:01):But in hindsight this is a bit silly, because these things are there in the constr anyways.
Pierre-Marie Pédrot (Feb 05 2022 at 18:02):What if we allowed the user to put arbitrary parameters there and preserve them until the kernel, instead of reinferring them?
Pierre-Marie Pédrot (Feb 05 2022 at 18:02):We would also display them when going the other way around, leading to a 1:1 bijection.
Pierre-Marie Pédrot (Feb 05 2022 at 18:03):(and similarly for the universe instance)
Pierre-Marie Pédrot (Feb 05 2022 at 18:04):Does it sound like a reasonable idea?
Gaëtan Gilbert (Feb 05 2022 at 18:05):try it and see how it goes
Pierre-Marie Pédrot (Feb 05 2022 at 18:08):What is "how"?
Pierre-Marie Pédrot (Feb 05 2022 at 18:08):I don't expect any trouble
Pierre-Marie Pédrot (Feb 05 2022 at 18:09):rather it's a design choice that we want to expose this to the user
Pierre-Marie Pédrot (Feb 05 2022 at 18:09):(it would also make explicit some pattern selection weirdnesses)
Hugo Herbelin (Feb 06 2022 at 09:29):Is what makes you hesitating the difference of status that parameters and indices would have in the in clause (terms for the former, binders for the latter)? If so, an alternative would be to write things like in I (A:=nat) (x:=0) y. That's a bit cumbersome but if it is mostly expected for the Set Printing All mode, that could be acceptable.
Otherwise, why not in I nat 0 y as well if the difference of status between parameters and indices is clearly documented.
Side question: in constructors, that would remain _ I guess?
Gaëtan Gilbert (Feb 06 2022 at 12:47):it should remain compatible with notations so that we can do in (x = y) so the := form may be too different
Matthieu Sozeau (Feb 06 2022 at 22:36):I think we should do it, maybe subject to an optional Set Printing option
Last updated: Oct 08 2024 at 14:01 UTC