Re: [isabelle] Invalid code when overriding code setup

Hi Lars,

> 1) The "String" theory introduces "char" as a "typedef", but omits the
> I think the lifting setup should be added to the "String" theory. I
> tried doing that, but unfortunately something broke in "Typerep" (of
> which I have no idea).


(currently in testing)

> 2) When importing "~~/src/HOL/Library/Code_Char", it seems to be
> impossible to override the code setup given there.

The assumption has always been that importing one of those funny Code_*
theories is the last word on a particular code setup.  Maybe localized
code declarations can lift that restriction in the future.

>I would have expected that a
> "code_datatype" statement overrides any previous "code_printing" for the
> same type constructor.

No.  "code_printing" is just fiddling with concrete syntax without a
deeper semantic notion behind.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.