Char
Characters
toNat32
let toNat32 : (c : Char) -> Nat32
Convert character c
to a word containing its Unicode scalar value.
fromNat32
let fromNat32 : (w : Nat32) -> Char
Convert w
to a character.
Traps if w
is not a valid Unicode scalar value.
Value w
is valid if, and only if, w < 0xD800 or (0xE000 ⇐ w and w ⇐ 0x10FFFF)
.