The reference holding `role`'s own leaf value: after replication it holds
the root value.
387def nativeCombineLeafReferenceFrom =
388 (lambda unrestricted role : Nat .
389 (lambda unrestricted tree : (family OrderedCombineTree) .
390 (eliminate
391 OrderedCombineTree
392 (lambda unrestricted current : (family OrderedCombineTree) .
393 (pi unrestricted base : Nat . (family CombineReference)))
394 tree
395 (branch
396 OrderedCombineLeaf
397 owner
398 .
399 (lambda unrestricted base : Nat . (combineReference owner base 0)))
400 (branch
401 OrderedCombineBranch
402 owner
403 left
404 right
405 leftResult
406 rightResult
407 .
408 (lambda unrestricted base : Nat .
409 (nat-eliminate
410 (lambda unrestricted flag : Nat . (family CombineReference))
411 (rightResult (naturalAdd base (combineNodeCount left)))
412 (lambda unrestricted prior : Nat .
413 (lambda unrestricted ignored : (family CombineReference) . (leftResult base)))
414 (combineContains role (combineLeaves left))))))))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.