Source/Packages

Data.UTF8

packages/foundation/standard/src/Data/UTF8.alpha

1,298 lines193 declarations53.6 KiBSHA-256 4bef3dfd330d

def · lines 1253–1287

encodeUTF8WithTelemetry

Full file
1253def encodeUTF8WithTelemetry =
1254  (lambda unrestricted codepoints : (family UTF8Codepoints) .
1255    (eliminate
1256      UTF8EncodeResult
1257      (lambda unrestricted current : (family UTF8EncodeResult) . (family UTF8EncodeExecutionResult))
1258      (encodeUTF8 codepoints)
1259      (branch
1260        UTF8EncodeSucceeded
1261        encoded
1262        .
1263        (constructor
1264          UTF8EncodeExecutionResult
1265          UTF8EncodeExecutionSucceeded
1266          encoded
1267          (utf8EncodeTelemetryFor
1268            codepoints
1269            (utf8CodepointsLength codepoints)
1270            (bytes-length encoded)
1271            zero
1272            zero)))
1273      (branch
1274        UTF8EncodeFailed
1275        code
1276        offset
1277        .
1278        (app
1279          (lambda unrestricted exactOffset : Nat .
1280            (constructor
1281              UTF8EncodeExecutionResult
1282              UTF8EncodeExecutionFailed
1283              code
1284              offset
1285              (utf8ErrorStableCode code)
1286              (utf8EncodeTelemetryFor codepoints exactOffset zero (succ zero) exactOffset)))
1287          (modelWord32ToNatural offset)))))

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.