[isabelle-dev] NEWS

[Florian Haftmann]

* 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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150910/cef51c4b/attachment.asc>