[isabelle-dev] NEWS

[Dmitriy Traytel]

Hi Florian,

while I very much welcome the simplified printing rules and your effort 
of unifying case_prod/split, I am not sure if adding a third alternative 
name is the way to go. The situation reminds me of the one depicted in [1].

Clearly, case_prod is the "right" name from the perspective of the 
(co)datatype package.

Dmitriy

[1] https://xkcd.com/927/

On 10.09.2015 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150910/05f53d43/attachment-0002.html>