[isabelle-dev] NEWS

[Tobias Nipkow]

I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). x+y" 
rather than "uncurry op +".

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
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150910/18931771/attachment.bin>