Third continuation of a four-byte sequence, completing the codepoint.
567def utf8MachineFourC =
568 (lambda unrestricted lead : Byte .
569 (lambda unrestricted b1 : Byte .
570 (lambda unrestricted b2 : Byte .
571 (lambda unrestricted b : Byte .
572 (lambda unrestricted rest : Bytes .
573 (lambda unrestricted pos : Nat .
574 (lambda unrestricted nextOffset : Nat .
575 (lambda unrestricted reversed : (family UTF8Codepoints) .
576 (nat-eliminate
577 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
578 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
579 (lambda unrestricted predecessor : Nat .
580 (lambda unrestricted induction : (family UTF8DecodeMachine) .
581 (utf8MachineEmit
582 (utf8CodepointFromFour lead b1 b2 b)
583 rest
584 nextOffset
585 reversed)))
586 (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.