552def jsonEncodeCodepointThen =
553 (lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
554 (lambda unrestricted codepoint : Nat .
555 (lambda unrestricted remaining : Bytes .
556 (eliminate
557 UTF8CodepointEncodeResult
558 (lambda unrestricted current : (family UTF8CodepointEncodeResult) .
559 (family JSONStringParseResult))
560 (utf8EncodeCodepoint
561 (constructor
562 UTF8Codepoint
563 UTF8CodepointValue
564 (modelWord32FromNaturalTruncated codepoint)))
565 (branch
566 UTF8CodepointEncoded
567 encoded
568 .
569 (jsonStringPrepend encoded (continuation remaining)))
570 (branch
571 UTF8CodepointRejected
572 code
573 .
574 (jsonStringFailure (constructor JSONErrorCode JSONUnicodeEscapeInvalid) remaining))))))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.