Second continuation of a four-byte sequence.
546def utf8MachineFourB =
547 (lambda unrestricted lead : Byte .
548 (lambda unrestricted b1 : Byte .
549 (lambda unrestricted b : Byte .
550 (lambda unrestricted rest : Bytes .
551 (lambda unrestricted pos : Nat .
552 (lambda unrestricted nextOffset : Nat .
553 (lambda unrestricted reversed : (family UTF8Codepoints) .
554 (nat-eliminate
555 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
556 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
557 (lambda unrestricted predecessor : Nat .
558 (lambda unrestricted induction : (family UTF8DecodeMachine) .
559 (utf8MachineGoing
560 rest
561 nextOffset
562 (constructor UTF8DecodePending UTF8PendingFourC lead b1 b)
563 reversed)))
564 (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.