Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Conversion Scala Char to Isabelle chars

view this post on Zulip Email Gateway (Aug 18 2022 at 19:06):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear all Isabelle users,

I am using Isabelle code generation towards Scala and my Isabelle code
is using strings, i.e. lists of chars. However, in the generated code I
only have Isabelle representation of chars using couple of hexadecimal
numbers (am I right ?) but no function to convert Scala chars to an
Isabelle one...

Is there something that I missed somewhere or do I have to write it by hand?

Thanks in advance,

Thomas

view this post on Zulip Email Gateway (Aug 18 2022 at 19:06):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Thomas,

you don't have to do much. In Scala, the String class has the function toList which converts a string to a character list.

Moreover, if you import in your theory "~~/src/HOL/Library/Code_Char_chr"
then, the Isabelle chars should be mapped to Scala characters.

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 19:06):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Le 10/02/12 16:45, René Thiemann a écrit :

Dear Thomas,

you don't have to do much. In Scala, the String class has the function toList which converts a string to a character list.

Moreover, if you import in your theory "~~/src/HOL/Library/Code_Char_chr"
then, the Isabelle chars should be mapped to Scala characters.

Thanks a lot René!

Best regards,

Thomas

Cheers,
René

Am 10.02.2012 um 16:33 schrieb Thomas Genet:

Dear all Isabelle users,

I am using Isabelle code generation towards Scala and my Isabelle code is using strings, i.e. lists of chars. However, in the generated code I only have Isabelle representation of chars using couple of hexadecimal numbers (am I right ?) but no function to convert Scala chars to an Isabelle one...

Is there something that I missed somewhere or do I have to write it by hand?

Thanks in advance,

Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet@irisa.fr
http://www.irisa.fr/celtique/genet

Last updated: Apr 18 2024 at 12:27 UTC