731def nativeRegionDestinationsValid =
732 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
733 (stdListFold
734 (family NativeRegionDestination)
735 Nat
736 (lambda unrestricted destination : (family NativeRegionDestination) .
737 (lambda unrestricted rest : Nat .
738 (eliminate
739 NativeRegionDestination
740 (lambda unrestricted current : (family NativeRegionDestination) . Nat)
741 destination
742 (branch
743 NativeRegionDestinationOf
744 ordinal
745 interval
746 offset
747 .
748 (naturalAnd
749 rest
750 (naturalAnd
751 (naturalLess (intervalBegin interval) (intervalEnd interval))
752 (naturalEqual
753 (nativeRegionCoveredBytes plan ordinal interval)
754 (intervalExtent interval))))))))
755 1))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.