[isabelle-dev] NEWS

[Florian Haftmann]

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

-------------- 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/f89c327b/attachment.sig>