567def resourceRouteAllowed =
568 (lambda unrestricted schedule : (family ResourceSchedule) .
569 (lambda unrestricted sourceRole : Nat .
570 (lambda unrestricted destinationRole : Nat .
571 (lambda unrestricted linkId : Nat .
572 (lambda unrestricted realization : Bytes .
573 (lambda unrestricted bytes : Nat .
574 (eliminate
575 StdOption
576 (lambda unrestricted current : (family StdOption Nat) . Nat)
577 (resourcePlacementForRole sourceRole (resourceSchedulePlacements schedule))
578 (branch StdNone . 0)
579 (branch
580 StdSome
581 source
582 .
583 (eliminate
584 StdOption
585 (lambda unrestricted current : (family StdOption Nat) . Nat)
586 (resourcePlacementForRole destinationRole (resourceSchedulePlacements schedule))
587 (branch StdNone . 0)
588 (branch
589 StdSome
590 destination
591 .
592 (naturalNonzero
593 (resourceCount
594 (family ResourceLink)
595 (lambda unrestricted link : (family ResourceLink) .
596 (naturalAnd
597 (naturalEqual (resourceLinkId link) linkId)
598 (naturalAnd
599 (naturalEqual (resourceLinkSource link) source)
600 (naturalAnd
601 (naturalEqual (resourceLinkDestination link) destination)
602 (naturalAnd
603 (bytes-equal (resourceLinkRealization link) realization)
604 (resourceFactAllows (resourceLinkEnvelope link) bytes))))))
605 (resourceGraphLinks (resourceScheduleGraph schedule))))))))))))))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.