952def utf8EncodeBuilderFold =
953 (lambda unrestricted codepoints : (family UTF8Codepoints) .
954 (eliminate
955 UTF8Codepoints
956 (lambda unrestricted current : (family UTF8Codepoints) . (family UTF8EncodeBuilderResult))
957 codepoints
958 (branch
959 UTF8CodepointsEnd
960 .
961 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderSucceeded (bytes-builder-empty)))
962 (branch
963 UTF8CodepointsNext
964 head
965 tail
966 induction
967 .
968 (eliminate
969 UTF8CodepointEncodeResult
970 (lambda unrestricted current : (family UTF8CodepointEncodeResult) .
971 (family UTF8EncodeBuilderResult))
972 (utf8EncodeCodepoint head)
973 (branch
974 UTF8CodepointEncoded
975 encoded
976 .
977 (eliminate
978 UTF8EncodeBuilderResult
979 (lambda unrestricted current : (family UTF8EncodeBuilderResult) .
980 (family UTF8EncodeBuilderResult))
981 induction
982 (branch
983 UTF8EncodeBuilderSucceeded
984 suffix
985 .
986 (constructor
987 UTF8EncodeBuilderResult
988 UTF8EncodeBuilderSucceeded
989 (bytes-builder-append (bytes-builder-chunk encoded) suffix)))
990 (branch
991 UTF8EncodeBuilderFailed
992 code
993 offset
994 .
995 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code (succ offset)))))
996 (branch
997 UTF8CodepointRejected
998 code
999 .
1000 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code zero))))))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.