Source/Packages

Data.UTF8

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

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

def · lines 1197–1215

utf8EncodeTelemetryFor

Full file
1197def utf8EncodeTelemetryFor =
1198  (lambda unrestricted codepoints : (family UTF8Codepoints) .
1199    (lambda unrestricted processed : Nat .
1200      (lambda unrestricted outputBytes : Nat .
1201        (lambda unrestricted failurePresent : Nat .
1202          (lambda unrestricted failureOrdinal : Nat .
1203            (constructor
1204              UTF8EncodeTelemetry
1205              UTF8EncodeTelemetryValue
1206              (utf8CodepointsLength codepoints)
1207              processed
1208              outputBytes
1209              (utf8CodepointsWidthCount utf8NaturalOne codepoints)
1210              (utf8CodepointsWidthCount utf8NaturalTwo codepoints)
1211              (utf8CodepointsWidthCount utf8NaturalThree codepoints)
1212              (utf8CodepointsWidthCount (byte-to-nat (byte 4)) codepoints)
1213              (utf8CodepointsInvalidCount codepoints)
1214              failurePresent
1215              failureOrdinal))))))

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.