[isabelle-dev] NEWS

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 10 12:48:50 CEST 2015

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}".


> 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.
>> 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150910/2defb8b2/attachment.sig>

More information about the isabelle-dev mailing list