239def nativePhysicalProgramComposeProgramPayloadBytes =
240 (lambda unrestricted program : (family NativePhysicalProgram) .
241 (eliminate NativePhysicalProgram
242 (lambda unrestricted current : (family NativePhysicalProgram) . Nat)
243 program
244 (branch NativePhysicalProgramValue
245 stateExtent resultSlots commands expected identity fallbacks .
246 (eliminate NativePhysicalCounts
247 (lambda unrestricted current : (family NativePhysicalCounts) . Nat)
248 (app nativePhysicalCommandsCounts commands)
249 (branch NativePhysicalCountsValue
250 commandCount systemCalls copies routines polls telemetry assertions
251 halts payloadBytes . payloadBytes)))))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.