AlphaGitHub
Source/Packages

Runtime.NativeCombine

packages/execution/src/Runtime/NativeCombine.alpha

874 lines55 declarations36.9 KiBSHA-256 10cc50beeee8
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 692–710

nativeCombineChain

Full file
The left-deep ordered sum of leaves 0..count-1 combined at `owner`: (((l0 + l1) + l2) + ...). Every transfer is between `owner` and a leaf, so it runs over a star whose centre is `owner`.
692def nativeCombineChain =
693  (lambda unrestricted owner : Nat .
694    (lambda unrestricted count : Nat .
695      (stdListFold
696        Nat
697        (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree))
698        (lambda unrestricted leaf : Nat .
699          (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
700            (lambda unrestricted acc : (family OrderedCombineTree) .
701              (next
702                (constructor
703                  OrderedCombineTree
704                  OrderedCombineBranch
705                  owner
706                  acc
707                  (constructor OrderedCombineTree OrderedCombineLeaf (succ leaf)))))))
708        (lambda unrestricted acc : (family OrderedCombineTree) . acc)
709        (stdListNaturalsBelow (naturalPredecessor count))
710        (constructor OrderedCombineTree OrderedCombineLeaf 0))))

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.