Re: [isabelle] Problems with linear orders and strings

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

thanks Florian for the pointers.

>> 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?

Unfortunately: yes.

theory Test
imports Char_ord Code_Char_chr

definition f where "f x \<equiv> (x :: char) <= x"
export_code f in Haskell file -

yields a similar error message as my own definition of <= on characters.

René Thiemann                    mailto:rene.thiemann at
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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