1378def dataBytesRenderHexWithin =
1379 (lambda unrestricted allocationLimit : Nat .
1380 (lambda unrestricted input : Bytes .
1381 (app
1382 (lambda unrestricted inputLength : Nat .
1383 (eliminate
1384 DataBytesCheckedNaturalResult
1385 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
1386 (family DataBytesResult))
1387 (dataBytesCheckedAddWithin
1388 allocationLimit
1389 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
1390 inputLength
1391 inputLength)
1392 (branch
1393 DataBytesCheckedNaturalSucceeded
1394 outputLength
1395 .
1396 (app
1397 (lambda unrestricted output : Bytes .
1398 (constructor
1399 DataBytesResult
1400 DataBytesSucceeded
1401 output
1402 (dataBytesTelemetry
1403 inputLength
1404 outputLength
1405 outputLength
1406 inputLength
1407 zero
1408 outputLength
1409 inputLength
1410 allocationLimit)))
1411 (bytes-builder-build (dataBytesRenderHexBuilder input))))
1412 (branch
1413 DataBytesCheckedNaturalFailed
1414 code
1415 .
1416 (constructor
1417 DataBytesResult
1418 DataBytesFailed
1419 code
1420 (dataBytesTelemetry
1421 inputLength
1422 inputLength
1423 zero
1424 zero
1425 zero
1426 zero
1427 zero
1428 allocationLimit)))))
1429 (bytes-length input))))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.