Continuations are forced only for the selected transition.
68def quotedChoose =
69 (lambda unrestricted condition : Nat .
70 (lambda unrestricted yes : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
71 (lambda unrestricted no : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
72 (app
73 (nat-eliminate
74 (lambda unrestricted flag : Nat .
75 (pi unrestricted force : Nat . (family QuotedLiteralResult)))
76 no
77 (lambda unrestricted predecessor : Nat .
78 (lambda unrestricted unused : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
79 yes))
80 condition)
81 zero))))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.