668def chCombineOperationAdmitted =
669 (lambda unrestricted role : Nat .
670 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) .
671 (eliminate
672 OrderedCombineOperation
673 (lambda unrestricted current : (family OrderedCombineOperation (family RegionFrameLayout)) .
674 Nat)
675 operation
676 (branch CombineReadLeaf destination . (chCombineReferenceAdmitted role destination))
677 (branch
678 CombineCopy
679 source
680 destination
681 .
682 (naturalAnd
683 (chCombineReferenceAdmitted role source)
684 (naturalAnd (chCombineReferenceAdmitted role destination) 1)))
685 (branch
686 CombineApply
687 left
688 right
689 destination
690 .
691 (naturalAnd
692 (chCombineReferenceAdmitted role left)
693 (naturalAnd
694 (chCombineReferenceAdmitted role right)
695 (naturalAnd (chCombineReferenceAdmitted role destination) 1))))
696 (branch CombinePrepare source frame . (chCombineReferenceAdmitted role source))
697 (branch CombineConsume frame destination . (chCombineReferenceAdmitted role destination)))))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.