Reachable logical slots only: unrelated participants consume no local arena.
399def combineLocalSlotsFrom =
400 (lambda unrestricted role : Nat .
401 (lambda unrestricted tree : (family OrderedCombineTree) .
402 (eliminate
403 OrderedCombineTree
404 (lambda unrestricted current : (family OrderedCombineTree) .
405 (pi unrestricted base : Nat . (family StdList Nat)))
406 tree
407 (branch
408 OrderedCombineLeaf
409 owner
410 .
411 (lambda unrestricted base : Nat .
412 (nat-eliminate
413 (lambda unrestricted flag : Nat . (family StdList Nat))
414 (constructor StdList StdListEmpty Nat)
415 (lambda unrestricted prior : Nat .
416 (lambda unrestricted ignored : (family StdList Nat) .
417 (constructor
418 StdList
419 StdListCons
420 Nat
421 (naturalMultiply 3 base)
422 (constructor StdList StdListEmpty Nat))))
423 (naturalEqual owner role))))
424 (branch
425 OrderedCombineBranch
426 owner
427 left
428 right
429 leftResult
430 rightResult
431 .
432 (lambda unrestricted base : Nat .
433 (let unrestricted rightBase =
434 (naturalAdd base (combineNodeCount left))
435 in
436 (let unrestricted node =
437 (naturalAdd rightBase (combineNodeCount right))
438 in
439 (stdListAppend
440 Nat
441 (leftResult base)
442 (stdListAppend
443 Nat
444 (rightResult rightBase)
445 (nat-eliminate
446 (lambda unrestricted flag : Nat . (family StdList Nat))
447 (constructor StdList StdListEmpty Nat)
448 (lambda unrestricted prior : Nat .
449 (lambda unrestricted ignored : (family StdList Nat) .
450 (constructor
451 StdList
452 StdListCons
453 Nat
454 (naturalMultiply 3 node)
455 (constructor
456 StdList
457 StdListCons
458 Nat
459 (naturalAdd (naturalMultiply 3 node) 1)
460 (constructor
461 StdList
462 StdListCons
463 Nat
464 (naturalAdd (naturalMultiply 3 node) 2)
465 (constructor StdList StdListEmpty Nat))))))
466 (naturalEqual owner role)))))))))))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.