AlphaGitHub
Source/Packages

Runtime.OrderedCombine

packages/execution/src/Runtime/OrderedCombine.alpha

329 lines62 declarations11.3 KiBSHA-256 c7d6a83584b8
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 118–137

combineLeaves

Full file
118def combineLeaves =
119  (lambda unrestricted tree : (family OrderedCombineTree) .
120    (eliminate
121      OrderedCombineTree
122      (lambda unrestricted current : (family OrderedCombineTree) . (family StdList Nat))
123      tree
124      (branch
125        OrderedCombineLeaf
126        owner
127        .
128        (constructor StdList StdListCons Nat owner (constructor StdList StdListEmpty Nat)))
129      (branch
130        OrderedCombineBranch
131        owner
132        left
133        right
134        leftResult
135        rightResult
136        .
137        (stdListAppend Nat leftResult rightResult))))

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.