`whenTrue` when the flag is nonzero, else `whenFalse`, at any type (the
one not chosen is not evaluated)
299def aosChoose =
300 (lambda erased result : Type 0 . (lambda unrestricted condition : Nat .
301 (lambda unrestricted whenTrue : result . (lambda unrestricted whenFalse : result .
302 (nat-eliminate (lambda unrestricted current : Nat . result) whenFalse
303 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : result . whenTrue))
304 condition)))))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.