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.
The only real difference is that we do not display parameters / universe instances of the return clause to the user.
In practice, we force syntactically parameters of the return clause to always be underscores.
But in hindsight this is a bit silly, because these things are there in the constr anyways.
What if we allowed the user to put arbitrary parameters there and preserve them until the kernel, instead of reinferring them?
We would also display them when going the other way around, leading to a 1:1 bijection.
(and similarly for the universe instance)
Does it sound like a reasonable idea?
try it and see how it goes
What is "how"?
I don't expect any trouble
rather it's a design choice that we want to expose this to the user
(it would also make explicit some pattern selection weirdnesses)
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?
it should remain compatible with notations so that we can do
in (x = y) so the := form may be too different
I think we should do it, maybe subject to an optional
Set Printing option
Last updated: Dec 05 2023 at 04:01 UTC