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 71–95

combineOwnersValid

Full file
71def combineOwnersValid =
72  (lambda unrestricted participants : Nat .
73    (lambda unrestricted tree : (family OrderedCombineTree) .
74      (eliminate
75        OrderedCombineTree
76        (lambda unrestricted current : (family OrderedCombineTree) . Nat)
77        tree
78        (branch OrderedCombineLeaf owner . (naturalLess owner participants))
79        (branch
80          OrderedCombineBranch
81          owner
82          left
83          right
84          leftResult
85          rightResult
86          .
87          (naturalAnd
88            leftResult
89            (naturalAnd
90              rightResult
91              (naturalAnd
92                (naturalOr
93                  (naturalEqual owner (combineOwner left))
94                  (naturalEqual owner (combineOwner right)))
95                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.