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
begin

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