Re: [isabelle] Problems with linear orders and strings



Hi René,

> 1) are there already theories which make char and string members of linorder

there are theories in HOL/Library, e.g. Char_ord and List_lexord and
List_Prefix -- note that strings are just char lists, no type on their own

> 2) I have defined my own class instance for char as follows:

> and then proven that this implementation satisfies the class conditions.
> Unfortunately, after loading Code_Char_chr I cannot export the code anymore
> since it is complains as follows:

Does this persists if you use the »official« Char_ord theory?

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.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.