First continuation of a four-byte sequence. `leadOffset` carries the lead's
offset for the overlong and out-of-range reports.
509def utf8MachineFourA =
510 (lambda unrestricted lead : Byte .
511 (lambda unrestricted leadOffset : Nat .
512 (lambda unrestricted b : Byte .
513 (lambda unrestricted rest : Bytes .
514 (lambda unrestricted pos : Nat .
515 (lambda unrestricted nextOffset : Nat .
516 (lambda unrestricted reversed : (family UTF8Codepoints) .
517 (nat-eliminate
518 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
519 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
520 (lambda unrestricted predecessor : Nat .
521 (lambda unrestricted induction : (family UTF8DecodeMachine) .
522 (nat-eliminate
523 (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine))
524 (nat-eliminate
525 (lambda unrestricted outOfRange : Nat . (family UTF8DecodeMachine))
526 (utf8MachineGoing
527 rest
528 nextOffset
529 (constructor UTF8DecodePending UTF8PendingFourB lead b)
530 reversed)
531 (lambda unrestricted rangePredecessor : Nat .
532 (lambda unrestricted rangeInduction : (family UTF8DecodeMachine) .
533 (utf8MachineFailAt
534 (constructor UTF8ErrorCode UTF8CodepointOutOfRange)
535 leadOffset)))
536 (utf8FlagAnd (byte-equal lead (byte 244)) (utf8ByteAtLeast b (byte 144))))
537 (lambda unrestricted overlongPredecessor : Nat .
538 (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) .
539 (utf8MachineFailAt
540 (constructor UTF8ErrorCode UTF8FourByteOverlong)
541 leadOffset)))
542 (utf8FlagAnd (byte-equal lead (byte 240)) (byte-less-than b (byte 144))))))
543 (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.