On 24.04.2013 16:18, Brian Huffman wrote:
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel <tray...@in.tum.de> wrote:
However, your example is still not printed as expected (assuming that the
output should be equal to the input in this case):
"(case x of (a, b) => λ(c, d). e) y"
Usually "prod_case" is printed as a tuple-lambda when partially
applied, and as a case expression when fully applied. So considering
that the underlying term in my example is "prod_case (λa b. prod_case
(λc d. e)) x y", the above output makes perfect sense.
I see. Previously, I though that "prod_case" is always supposed to be
printed as a lambda with a pattern and the fact that it is printed as a
case expression sometimes is a coincidence caused by the order in which
syntax translations are applied. But your explanation makes sense and
results in less work for me :-)
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
