First continuation of a three-byte sequence. `leadOffset` is the lead's byte
offset (overlong and surrogate are reported there); `pos` is this byte's.
454def utf8MachineThreeA =
455 (lambda unrestricted lead : Byte .
456 (lambda unrestricted leadOffset : Nat .
457 (lambda unrestricted b : Byte .
458 (lambda unrestricted rest : Bytes .
459 (lambda unrestricted pos : Nat .
460 (lambda unrestricted nextOffset : Nat .
461 (lambda unrestricted reversed : (family UTF8Codepoints) .
462 (nat-eliminate
463 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
464 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
465 (lambda unrestricted predecessor : Nat .
466 (lambda unrestricted induction : (family UTF8DecodeMachine) .
467 (nat-eliminate
468 (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine))
469 (nat-eliminate
470 (lambda unrestricted surrogate : Nat . (family UTF8DecodeMachine))
471 (utf8MachineGoing
472 rest
473 nextOffset
474 (constructor UTF8DecodePending UTF8PendingThreeB lead b)
475 reversed)
476 (lambda unrestricted surrogatePredecessor : Nat .
477 (lambda unrestricted surrogateInduction : (family UTF8DecodeMachine) .
478 (utf8MachineFailAt
479 (constructor UTF8ErrorCode UTF8SurrogateCodepoint)
480 leadOffset)))
481 (utf8FlagAnd (byte-equal lead (byte 237)) (utf8ByteAtLeast b (byte 160))))
482 (lambda unrestricted overlongPredecessor : Nat .
483 (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) .
484 (utf8MachineFailAt
485 (constructor UTF8ErrorCode UTF8ThreeByteOverlong)
486 leadOffset)))
487 (utf8FlagAnd (byte-equal lead (byte 224)) (byte-less-than b (byte 160))))))
488 (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.