Codepoint words are composed from the byte bits directly (D17): no natural
arithmetic, so a decoded character costs a handful of byte operations
instead of a fold over the codepoint's value.
320def utf8CodepointWord =
321 (lambda unrestricted b0 : Byte .
322 (lambda unrestricted b1 : Byte .
323 (lambda unrestricted b2 : Byte .
324 (constructor
325 UTF8Codepoint
326 UTF8CodepointValue
327 (constructor ModelWord32 ModelWord32Value b0 b1 b2 (byte 0))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.