Thanks!
??, 21 ??? 2020 ?. ? 14:36, David Matthews <David.Matthews at prolingua.co.uk>:
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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml