369def lifetimesValid =
370 (lambda unrestricted lifetimes : (family Lifetimes) .
371 (eliminate
372 Lifetimes
373 (lambda unrestricted current : (family Lifetimes) . Nat)
374 lifetimes
375 (branch LifetimesEnd . (succ zero))
376 (branch LifetimesNext head tail ih_tail . (naturalFlagAnd (lifetimeIsValid head) ih_tail))))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.