> I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). > x+y" rather than "uncurry op +".
Okay, this is really unpleasant. Thanks for reporting this. Florian > > Tobias > > On 10/09/2015 12:48, Florian Haftmann wrote: >> Hi Andreas, >> >>> I noticed that the new printing interacts strangely with set >>> comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as >>> "Collect (uncurry P)" which I find rather hard to read. Are you aware of >>> this effect and could you please restore the former situation? >> >> this is on my to-do list, together with other binder-related issues like >> "{p. case p of (x, y) => P x y}". >> >> Florian >> >>> >>> Best, >>> Andreas >>> >>> On 10/09/15 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 > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev