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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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