<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Florian,<br>
<br>
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].<br>
<br>
Clearly, case_prod is the "right" name from the perspective of the
(co)datatype package.<br>
<br>
Dmitriy<br>
<br>
[1] <a class="moz-txt-link-freetext" href="https://xkcd.com/927/">https://xkcd.com/927/</a><br>
<br>
On 10.09.2015 12:02, Florian Haftmann wrote:<br>
</div>
<blockquote cite="mid:55F15550.7070100@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">* 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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>