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).

see

http://isabelle.in.tum.de/repos/testboard/rev/f16db95a5a20
http://isabelle.in.tum.de/repos/testboard/rev/3885322d8f57

(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,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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