noschinl at in.tum.de
Thu Sep 10 13:46:49 CEST 2015
On 10.09.2015 12:19, Dmitriy Traytel wrote:
> Hi Florian,
> while I very much welcome the simplified printing rules and your effort
> of unifying case_prod/split, I am not sure if adding a third alternative
> name is the way to go. The situation reminds me of the one depicted in .
> Clearly, case_prod is the "right" name from the perspective of the
> (co)datatype package.
I also prefer a name following the usual case_<type> convention over a
special case for type prod.
>> b) partially applied with explicit double lambda abstraction in
>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
>> c) partially applied with eta-contracted body term "uncurry f":
>> no special syntax, plain "uncurry" combinator.
This does not seem to work right now; case b) is printed like c) if the
body is eta-contractable (but not eta-contracted).
>> This schema emerged after some experimentation and seems to be a
>> convenient compromise. The longer perspective is to overcome the
>> case_prod/split schism eventually and consolidate theorem names accordingly.
What is the problem with converging to the default names created by the
new datatype package?
More information about the isabelle-dev