Hi,
No, it's correct. Char.toString is defined to return a printable
representation of the character, escaping if necessary. To convert a
char to a single character string use String.str.
> val c = Char.toString #"\"";
val c = "\\\"": string
> val c = String.str #"\"";
val c = "\"": string
>
David
On 21/05/2020 12:18, Kostirya wrote:
Hello.
Is it bug?
Poly/ML 5.8 Release
val c = Char.toString #"\"";
val c = "\\\"": string
explode c;
val it = [#"\\", #"\""]: char list
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
