3564def finishBinderForm =
3565 (lambda unrestricted formTag : Nat .
3566 (lambda unrestricted quantityTag : Nat .
3567 (lambda unrestricted binderSpelling : Bytes .
3568 (lambda unrestricted domain : (family Term) .
3569 (lambda unrestricted body : (family Term) .
3570 (lambda unrestricted remaining : (family TermList) .
3571 (eliminate
3572 TermList
3573 (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3574 remaining
3575 (branch
3576 TermListEnd
3577 .
3578 (nat-eliminate
3579 (lambda unrestricted value : Nat . (family TermDecodeResult))
3580 (constructor
3581 TermDecodeResult
3582 TermDecoded
3583 (constructor Term Lambda quantityTag binderSpelling domain body))
3584 (lambda unrestricted predecessor : Nat .
3585 (lambda unrestricted induction : (family TermDecodeResult) .
3586 (constructor
3587 TermDecodeResult
3588 TermDecoded
3589 (constructor Term Pi quantityTag binderSpelling domain body))))
3590 formTag))
3591 (branch
3592 TermListNext
3593 listedTerm
3594 listedRest
3595 ih_listedRest
3596 .
3597 (binderDecodeFailed binderSyntaxFailureCode)))))))))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.