3705def decodeBinderQuantity =
3706 (lambda unrestricted formTag : Nat .
3707 (lambda unrestricted quantityResult : (family QuantityDecodeResult) .
3708 (lambda unrestricted remaining : (family TermList) .
3709 (eliminate
3710 QuantityDecodeResult
3711 (lambda unrestricted result : (family QuantityDecodeResult) . (family TermDecodeResult))
3712 quantityResult
3713 (branch
3714 QuantityDecoded
3715 quantityTag
3716 .
3717 (eliminate
3718 TermList
3719 (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3720 remaining
3721 (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode))
3722 (branch
3723 TermListNext
3724 binderTerm
3725 afterName
3726 ih_afterName
3727 .
3728 (eliminate
3729 TermSpellingResult
3730 (lambda unrestricted result : (family TermSpellingResult) .
3731 (family TermDecodeResult))
3732 (termSpelling binderTerm)
3733 (branch
3734 TermSpellingDecoded
3735 binderSpelling
3736 .
3737 (decodeBinderAfterName formTag quantityTag binderSpelling afterName))
3738 (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode))))))
3739 (branch QuantityInvalid . (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.