[isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package
traytel at in.tum.de
Wed Apr 24 11:52:58 CEST 2013
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) ⇒ λ(c, d). e) y"
I think, the proper resolution to this is to have an uncheck phase for
turning "prod_case e" intro λ(x, y). e x y" before the case translation
uncheck phase. Maybe Makarius or Stefan could comment on this. Then, I
could have a look.
On 24.04.2013 02:10, Brian Huffman wrote:
> 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))))
> :: "'e"
> I assume this is a result of the recent changes to the handling of
> case expressions?
> - Brian
> On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel <traytel at in.tum.de> wrote:
>> * Nested case expressions are now translated in a separate check
>> phase rather than during parsing. The data for case combinators
>> is separated from the datatype package. The declaration attribute
>> "case_tr" can be used to register new case combinators:
>> declare [[case_translation case_combinator constructor1 ... constructorN]]
>> This refers to Isabelle/bdaa1582dc8b
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
More information about the isabelle-dev