`chosen` when the flag is nonzero, else `otherwise`
372def coppeliusStepsWhen =
373 (lambda unrestricted flag : Nat .
374 (lambda unrestricted chosen : (family NvidiaPlanHostSteps) .
375 (lambda unrestricted otherwise : (family NvidiaPlanHostSteps) .
376 (nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostSteps)) otherwise
377 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NvidiaPlanHostSteps) . chosen))
378 flag))))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.