Second continuation of a three-byte sequence, completing the codepoint.
491def utf8MachineThreeB =
492 (lambda unrestricted lead : Byte .
493 (lambda unrestricted b1 : Byte .
494 (lambda unrestricted b : Byte .
495 (lambda unrestricted rest : Bytes .
496 (lambda unrestricted pos : Nat .
497 (lambda unrestricted nextOffset : Nat .
498 (lambda unrestricted reversed : (family UTF8Codepoints) .
499 (nat-eliminate
500 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
501 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
502 (lambda unrestricted predecessor : Nat .
503 (lambda unrestricted induction : (family UTF8DecodeMachine) .
504 (utf8MachineEmit (utf8CodepointFromThree lead b1 b) rest nextOffset reversed)))
505 (utf8ContinuationValid b)))))))))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.