472def combineReferenceIndex =
473 (lambda unrestricted role : Nat .
474 (lambda unrestricted tree : (family OrderedCombineTree) .
475 (lambda unrestricted reference : (family CombineReference) .
476 (nat-eliminate
477 (lambda unrestricted flag : Nat . (family StdOption Nat))
478 (constructor StdOption StdNone Nat)
479 (lambda unrestricted prior : Nat .
480 (lambda unrestricted ignored : (family StdOption Nat) .
481 (app
482 (eliminate
483 StdList
484 (lambda unrestricted current : (family StdList Nat) .
485 (pi unrestricted index : Nat . (family StdOption Nat)))
486 (combineLocalSlots role tree)
487 (branch
488 StdListEmpty
489 .
490 (lambda unrestricted index : Nat . (constructor StdOption StdNone Nat)))
491 (branch
492 StdListCons
493 head
494 tail
495 induction
496 .
497 (lambda unrestricted index : Nat .
498 (nat-eliminate
499 (lambda unrestricted flag : Nat . (family StdOption Nat))
500 (induction (naturalAdd index 1))
501 (lambda unrestricted prior : Nat .
502 (lambda unrestricted ignored : (family StdOption Nat) .
503 (constructor StdOption StdSome Nat index)))
504 (naturalEqual head (combineReferenceSlot reference))))))
505 0)))
506 (naturalEqual role (combineReferenceOwner reference))))))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.