Hi Florian,
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?
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
