src/Unicode has a fairly pure implementation of UTF-16 and UTF-8, but it uses bit vector types and doesn't use char or string at all. We definitely need a standard library that does (and the incoming JSON PR does itself, since it needs to encode a string in UTF-8), although this means we'll need at least some Dafny code that is duplicated to account for the difference in behavior from --unicode-char.
src/Unicode
has a fairly pure implementation of UTF-16 and UTF-8, but it uses bit vector types and doesn't usechar
orstring
at all. We definitely need a standard library that does (and the incoming JSON PR does itself, since it needs to encode astring
in UTF-8), although this means we'll need at least some Dafny code that is duplicated to account for the difference in behavior from--unicode-char
.