The target owns the step's arithmetic and refusal. Logical position advances
only after that callback returns successfully; capture occurs after all steps.
533def niRoundsAt =
534 (lambda unrestricted stateAt : Nat .
535 (lambda unrestricted steps : Nat .
536 (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
537 (lambda unrestricted tail : (family NativePhysicalCommands) .
538 (nativeLaunchRecipeCommand
539 (constructor
540 NativePhysicalOperation
541 NativePhysicalRepeatBeginCounted
542 (nativeLaunchRecipeImmediate steps))
543 b"independent-repeat"
544 (step
545 (niAdvanceAt
546 stateAt
547 (nativeLaunchRecipeCommand
548 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
549 b"independent-repeat-end"
550 tail))))))))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.