The extent of the record nativePhysicalImageEncodeCommand writes for a
command, measured from that encoding (so it cannot drift from the record
layout); 0 for a command that cannot be encoded. Shared routine code is a
property of a whole image, not of one command, and is not applied here.
1417def nativePhysicalImageCommandExtent =
1418 (lambda unrestricted command : (family NativePhysicalCommand) .
1419 (eliminate
1420 NativePhysicalEncodedCommandResult
1421 (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) . Nat)
1422 (nativePhysicalImageEncodeCommand command)
1423 (branch
1424 NativePhysicalCommandEncoded
1425 encoded
1426 .
1427 (eliminate
1428 NativePhysicalEncodedCommand
1429 (lambda unrestricted current : (family NativePhysicalEncodedCommand) . Nat)
1430 encoded
1431 (branch NativePhysicalEncodedCommandValue bytes payloadBytes auxiliaryBytes errorBytes . (bytes-length bytes))))
1432 (branch NativePhysicalCommandEncodingFailed error . zero)))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.