utf16 encoding

Stream: Is there code for X?

[tristanC]

I am looking for a function Char -> Fin 8 × Fin 8 to convert an unicode character to its utf16 big endian representation.

@loogle "utf16"

[loogle]

:exclamation: unknown identifier 'utf16'
Did you mean "utf16"?

[tristanC]

It's not total, but that seems to work for my use case :)

def Char.toUTF16BE (c : Char) : Option (UInt8 × UInt8) :=
  if c.val < 0x10000 then
    let c1 := UInt32.shiftRight c.val 8
    let c2 := UInt32.land c.val 0xff
    some (c1.toUInt8, c2.toUInt8)
  else none

[Eric Wieser]

I think the premise is wrong here: the type should be Char -> List UInt16 or similar because utf16 is a variable length encoding