Sounds good to me. Dmitriy
On 22.09.2015 16:20, Florian Haftmann wrote:
So, the direction is going towards prod_case. If this is settled, the consequences are: * Abbreviation »uncurry« will disappear again. * Abbreviation »split« will disappear finally (using the distribution and AFP as indicator whether this is »now« or »later«). * Theorem names contain »prod_case« instead of »split«; the latter are retained as aliasses, but documentation etc. is updated to prefer the first version. * There is no way to have something like »curry (uncurry f) = f« printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f x y) = f« by default. Any headache with this? Florian Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: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. Dmitriy [1] https://xkcd.com/927/ On 10.09.2015 12:02, Florian Haftmann wrote:* Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; 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 aims for maximum readability in a given subterm. INCOMPATIBILITY. This refers to e6b1236f9b3d. 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. The next step after this initial cleanup is to tackle the »let (a, b) = … in …« issue. Florian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
