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 [1]. > > 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? -- Laras _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev