AlphaGitHub
Source/Packages

Compiler.Planning.OrderedCombine

packages/compiler/planning/src/Compiler/Planning/OrderedCombine.alpha

832 lines26 declarations41.4 KiBSHA-256 69f52e43e720
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 97–112

combineTreeAdmitted

Full file
97def combineTreeAdmitted =
98  (lambda unrestricted participants : Nat .
99    (lambda unrestricted tree : (family OrderedCombineTree) .
100      (naturalAnd
101        (naturalNonzero participants)
102        (naturalAnd
103          (naturalLessOrEqual participants regionFrameWordLimit)
104          (naturalAnd
105            (combineOwnersValid participants tree)
106            (naturalAnd
107              (combineDistinct (combineLeaves tree))
108              (naturalAnd
109                (naturalLessOrEqual
110                  (combineNodeCount tree)
111                  (naturalDivideUnchecked regionFrameWordLimit 3))
112                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.