a verdict code: 0 when `first` is 0 (passed), else `first` -- the next
check is not evaluated once one has failed
294def aosThen =
295 (lambda unrestricted first : Nat . (lambda unrestricted next : Nat . (naturalSelect first first next)))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.