1 when f 0, f 1, ..., f (count - 1) are all nonzero, else 0: a bounded
universal verdict the checker can compute. With a statement for every
f (count + b), Std.Equality.stdNaturalAllBelowSound turns it into a
statement for every natural -- a finite region decided by computation, the
rest by an argument over an open offset.
290def naturalAllBelow =
291 (lambda unrestricted count : Nat .
292 (lambda unrestricted f : (pi unrestricted index : Nat . Nat) .
293 (naturalIsZero (naturalFailuresBelow count f))))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.