---- admission ----
569def nativeCombineLocalAdmitted =
570 (lambda unrestricted placement : (family NativeCombinePlacement) .
571 (lambda unrestricted role : Nat .
572 (let unrestricted placement =
573 (nativeCombineForPlacementRole placement role)
574 in
575 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
576 (eliminate
577 OrderedCombineOperation
578 (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
579 Nat)
580 operation
581 (branch
582 CombineReadLeaf
583 destination
584 .
585 (nativeCombineReferenceValid placement destination))
586 (branch
587 CombineCopy
588 source
589 destination
590 .
591 (naturalAnd
592 (nativeCombineReferenceValid placement source)
593 (nativeCombineReferenceValid placement destination)))
594 (branch
595 CombineApply
596 left
597 right
598 destination
599 .
600 (naturalAnd
601 (nativeCombineReferenceValid placement left)
602 (naturalAnd
603 (nativeCombineReferenceValid placement right)
604 (nativeCombineReferenceValid placement destination))))
605 (branch
606 CombinePrepare
607 source
608 identity
609 .
610 (naturalAnd
611 (nativeCombineReferenceValid placement source)
612 (naturalLess
613 (nativeCombineFrameIndex placement identity)
614 (nativeCombineFrameCount placement))))
615 (branch
616 CombineConsume
617 identity
618 destination
619 .
620 (naturalAnd
621 (nativeCombineReferenceValid placement destination)
622 (naturalLess
623 (nativeCombineFrameIndex placement identity)
624 (nativeCombineFrameCount placement)))))))))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.