Decodes one descriptor at its fixed manifest offset.
607def nativePhysicalEmbeddedDescriptorAt =
608 (lambda unrestricted manifestBytes : Bytes .
609 (lambda unrestricted descriptorOffset : Nat .
610 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
611 (constructor
612 NativePhysicalEmbeddedDescriptor
613 NativePhysicalEmbeddedDescriptorValue
614 kind
615 (nativePhysicalEmbeddedWord32At
616 manifestBytes
617 (naturalAdd descriptorOffset (byte-to-nat (byte 4))))
618 (nativePhysicalEmbeddedWord32At
619 manifestBytes
620 (naturalAdd descriptorOffset (byte-to-nat (byte 8))))
621 (nativePhysicalEmbeddedSliceOrEmpty
622 manifestBytes
623 (naturalAdd descriptorOffset (byte-to-nat (byte 12)))
624 nativePhysicalEmbeddedIdentityLength)
625 (nativePhysicalEmbeddedSliceOrEmpty
626 manifestBytes
627 (naturalAdd descriptorOffset (byte-to-nat (byte 76)))
628 nativePhysicalEmbeddedDigestLength)))))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.