Second byte of a two-byte sequence at offset `pos`.
437def utf8MachineTwo =
438 (lambda unrestricted lead : Byte .
439 (lambda unrestricted b : Byte .
440 (lambda unrestricted rest : Bytes .
441 (lambda unrestricted pos : Nat .
442 (lambda unrestricted nextOffset : Nat .
443 (lambda unrestricted reversed : (family UTF8Codepoints) .
444 (nat-eliminate
445 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
446 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
447 (lambda unrestricted predecessor : Nat .
448 (lambda unrestricted induction : (family UTF8DecodeMachine) .
449 (utf8MachineEmit (utf8CodepointFromTwo lead b) rest nextOffset reversed)))
450 (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.