Bounded exact slice used by the manifest decoder. Empty means failure;
admitted components are non-empty, so the sentinel is unambiguous.
573def nativePhysicalEmbeddedSliceOrEmpty =
574 (lambda unrestricted input : Bytes .
575 (lambda unrestricted offset : Nat .
576 (lambda unrestricted length : Nat .
577 (eliminate
578 DataBytesSliceResult
579 (lambda unrestricted current : (family DataBytesSliceResult) . Bytes)
580 (dataBytesSlice input offset length)
581 (branch
582 DataBytesSliceSucceeded
583 slice
584 telemetry
585 .
586 (eliminate
587 DataBytesResult
588 (lambda unrestricted current : (family DataBytesResult) . Bytes)
589 (dataBytesSliceToBytes slice)
590 (branch DataBytesSucceeded value materialTelemetry . value)
591 (branch DataBytesFailed code materialTelemetry . b"")))
592 (branch DataBytesSliceFailed code telemetry . b"")))))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.