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
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?
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 uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and