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
I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).
term (λ(a, b) (c, d). e) x y
case_guard True x
(case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e
case_nil)
y
:: 'e
I assume this is a result of the recent changes
Hi Brian
thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense
that internal constants (like case_guard) are not visible anymore.
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)
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote:
Hi Brian
thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense that
internal constants (like case_guard) are not visible anymore.
Thanks for taking care of this so quickly!
However, your example is
Hi Brian,
this is indeed somehow complicated.
Almost everything in the new shallow syntax translation and in the new
check phase destructs and constructs the function type. An example is
the print translation case_tr' in ~/src/HOL/Tools/case_translation.ML
which relies on
It would be nice to get HOLCF case combinators working with this new
system, as the parsing for HOLCF case expressions has been a bit
broken for some time.
Can case combinators and constructor functions with
continuous-function types be made to work with the case_tr (or
case_translation?)
