Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

2013-11-28 Thread Florian Haftmann
Hi Andreas René, a) Char_ord and List_lexord are not tied together, i.e., a user could import List_lexord, but not Char_ord, define his own version of order on String.literal and the generated Haskell code compiles, but it is unsound (even without any further adaptations by the user). One

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

2013-11-28 Thread Andreas Lochbihler
Hi Florian, a) Char_ord and List_lexord are not tied together, i.e., a user could import List_lexord, but not Char_ord, define his own version of order on String.literal and the generated Haskell code compiles, but it is unsound (even without any further adaptations by the user). One could

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

2013-11-20 Thread Andreas Lochbihler
Hi René and Florian (and other experts in code generation), I move this thread from users to dev because it is now getting into detailed discussions and commit ids. I've moved my setup for String.literal from Containers to the distribution and pushed the changes to testboard), but I realised