405def participantSelectUnchecked =
406 (lambda unrestricted index : (family ParticipantIndex) .
407 (eliminate
408 ParticipantIndex
409 (lambda unrestricted current : (family ParticipantIndex) .
410 (pi unrestricted ordinal : Nat . Nat))
411 index
412 (branch
413 ParticipantStrideIndex
414 bounds
415 stride
416 .
417 (lambda unrestricted ordinal : Nat .
418 (naturalAdd (participantBoundsLower bounds) (naturalMultiply ordinal stride))))
419 (branch
420 ParticipantRepeatIndex
421 bounds
422 stride
423 inner
424 induction
425 .
426 (lambda unrestricted ordinal : Nat .
427 (naturalAdd
428 (naturalMultiply (naturalDivideUnchecked ordinal (participantCountOf inner)) stride)
429 (induction (naturalModuloUnchecked ordinal (participantCountOf inner))))))
430 (branch
431 ParticipantJoinIndex
432 bounds
433 left
434 right
435 leftResult
436 rightResult
437 .
438 (lambda unrestricted ordinal : Nat .
439 (nat-eliminate
440 (lambda unrestricted flag : Nat . Nat)
441 (rightResult (naturalSaturatingSubtract ordinal (participantCountOf left)))
442 (lambda unrestricted prior : Nat .
443 (lambda unrestricted ignored : Nat . (leftResult ordinal)))
444 (naturalLess ordinal (participantCountOf 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.