Branches are suspended: the evaluator is strict in application arguments.
Calling the continuation in both value arguments would double the remaining
validation work at each byte, even when only one branch is selected.
529def integerLiteralChooseSyntax =
530 (lambda unrestricted condition : Nat .
531 (lambda unrestricted whenTrue : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
532 (lambda unrestricted whenFalse : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
533 (app
534 (nat-eliminate
535 (lambda unrestricted current : Nat .
536 (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)))
537 whenFalse
538 (lambda unrestricted predecessor : Nat .
539 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
540 whenTrue))
541 condition)
542 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.