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}". FlorianBest, 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
