Admission stops at the first named refusal; the remaining plan stays lazy.
509def combineRequire =
510 (lambda erased value : Type 0 .
511 (lambda unrestricted flag : Nat .
512 (lambda unrestricted failure : (family OrderedCombineFailure) .
513 (lambda unrestricted next : (family StdResult (family OrderedCombineFailure) value) .
514 (nat-eliminate
515 (lambda unrestricted current : Nat .
516 (family StdResult (family OrderedCombineFailure) value))
517 (constructor StdResult StdFailure (family OrderedCombineFailure) value failure)
518 (lambda unrestricted prior : Nat .
519 (lambda unrestricted ignored : (family StdResult (family OrderedCombineFailure) value) .
520 next))
521 flag)))))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.