48def modelWord32Select =
49 (lambda unrestricted condition : Nat .
50 (lambda unrestricted whenTrue : (family ModelWord32) .
51 (lambda unrestricted whenFalse : (family ModelWord32) .
52 (nat-eliminate
53 (lambda unrestricted current : Nat . (family ModelWord32))
54 whenFalse
55 (lambda unrestricted predecessor : Nat .
56 (lambda unrestricted induction : (family ModelWord32) . whenTrue))
57 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.