5659def applicationSpineLength =
5660 (lambda unrestricted term : (family Term) .
5661 (eliminate
5662 Term
5663 (lambda unrestricted value : (family Term) . Nat)
5664 term
5665 (branch Variable spelling . zero)
5666 (branch Universe level . zero)
5667 (branch NaturalType . zero)
5668 (branch NaturalZero . zero)
5669 (branch NaturalLiteral naturalLiteralValue . zero)
5670 (branch NaturalSuccessor predecessor ih_predecessor . zero)
5671 (branch Application function argument ih_function ih_argument . (succ ih_function))
5672 (branch NaturalArithmetic operation function argument ih_function ih_argument . zero)
5673 (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . zero)
5674 (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . zero)
5675 (branch BytesType . zero)
5676 (branch BytesLiteral bytesValue . zero)
5677 (branch ByteType . zero)
5678 (branch ByteLiteral byteValue . zero)
5679 (branch TermSequenceEnd . zero)
5680 (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . zero)
5681 (branch
5682 TermEliminatorBranch
5683 constructorSpelling
5684 binderNames
5685 body
5686 ih_binderNames
5687 ih_body
5688 .
5689 zero)
5690 (branch FamilyApplication familySpelling familyArguments ih_familyArguments . zero)
5691 (branch
5692 ConstructorApplication
5693 familySpelling
5694 constructorSpelling
5695 constructorArguments
5696 ih_constructorArguments
5697 .
5698 zero)
5699 (branch
5700 Eliminator
5701 eliminatedFamilySpelling
5702 motive
5703 scrutinee
5704 branches
5705 ih_motive
5706 ih_scrutinee
5707 ih_branches
5708 .
5709 zero)
5710 (branch Match family scrutinee branches ih_scrutinee ih_branches . zero)
5711 (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)
5712 (branch IntegerLiteral integerLiteralSpelling . zero)
5713 (branch RecordConstruction name origin bindings ih_bindings . zero)
5714 (branch RecordAssignment name origin value ih_value . zero)
5715 (branch RecordProjection name field origin value ih_value . zero)
5716 (branch RecordUpdate name origin value bindings ih_value ih_bindings . zero)
5717 (branch
5718 LocalLet
5719 quantity
5720 binder
5721 hasAnnotation
5722 annotation
5723 value
5724 body
5725 ih_annotation
5726 ih_value
5727 ih_body
5728 .
5729 zero)
5730 (branch DoBlock effects result body ih_effects ih_result ih_body . zero)
5731 (branch
5732 DoStep
5733 named
5734 quantity
5735 binder
5736 computation
5737 continuation
5738 ih_computation
5739 ih_continuation
5740 .
5741 zero)
5742 (branch DoReturn value ih_value . 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.