2566def termApplicationSpine =
2567 (lambda unrestricted term : (family Term) .
2568 (eliminate
2569 Term
2570 (lambda unrestricted value : (family Term) . (family TermApplicationSpine))
2571 term
2572 (branch
2573 Variable
2574 spelling
2575 .
2576 (constructor
2577 TermApplicationSpine
2578 TermApplicationSpineValue
2579 (constructor Term Variable spelling)
2580 (constructor TermList TermListEnd)))
2581 (branch
2582 Universe
2583 level
2584 .
2585 (constructor
2586 TermApplicationSpine
2587 TermApplicationSpineValue
2588 (constructor Term Universe level)
2589 (constructor TermList TermListEnd)))
2590 (branch
2591 NaturalType
2592 .
2593 (constructor
2594 TermApplicationSpine
2595 TermApplicationSpineValue
2596 (constructor Term NaturalType)
2597 (constructor TermList TermListEnd)))
2598 (branch
2599 NaturalZero
2600 .
2601 (constructor
2602 TermApplicationSpine
2603 TermApplicationSpineValue
2604 (constructor Term NaturalZero)
2605 (constructor TermList TermListEnd)))
2606 (branch
2607 NaturalLiteral
2608 value
2609 .
2610 (constructor
2611 TermApplicationSpine
2612 TermApplicationSpineValue
2613 (constructor Term NaturalLiteral value)
2614 (constructor TermList TermListEnd)))
2615 (branch
2616 NaturalSuccessor
2617 predecessor
2618 ih
2619 .
2620 (constructor
2621 TermApplicationSpine
2622 TermApplicationSpineValue
2623 (constructor Term NaturalSuccessor predecessor)
2624 (constructor TermList TermListEnd)))
2625 (branch
2626 Application
2627 function
2628 argument
2629 ih_function
2630 ih_argument
2631 .
2632 (appendSpineArgument ih_function argument))
2633 (branch
2634 NaturalArithmetic
2635 operation
2636 function
2637 argument
2638 ih_function
2639 ih_argument
2640 .
2641 (constructor
2642 TermApplicationSpine
2643 TermApplicationSpineValue
2644 (constructor Term NaturalArithmetic operation function argument)
2645 (constructor TermList TermListEnd)))
2646 (branch
2647 Lambda
2648 quantity
2649 binder
2650 domain
2651 body
2652 ih_domain
2653 ih_body
2654 .
2655 (constructor
2656 TermApplicationSpine
2657 TermApplicationSpineValue
2658 (constructor Term Lambda quantity binder domain body)
2659 (constructor TermList TermListEnd)))
2660 (branch
2661 Pi
2662 quantity
2663 binder
2664 domain
2665 body
2666 ih_domain
2667 ih_body
2668 .
2669 (constructor
2670 TermApplicationSpine
2671 TermApplicationSpineValue
2672 (constructor Term Pi quantity binder domain body)
2673 (constructor TermList TermListEnd)))
2674 (branch
2675 BytesType
2676 .
2677 (constructor
2678 TermApplicationSpine
2679 TermApplicationSpineValue
2680 (constructor Term BytesType)
2681 (constructor TermList TermListEnd)))
2682 (branch
2683 BytesLiteral
2684 value
2685 .
2686 (constructor
2687 TermApplicationSpine
2688 TermApplicationSpineValue
2689 (constructor Term BytesLiteral value)
2690 (constructor TermList TermListEnd)))
2691 (branch
2692 ByteType
2693 .
2694 (constructor
2695 TermApplicationSpine
2696 TermApplicationSpineValue
2697 (constructor Term ByteType)
2698 (constructor TermList TermListEnd)))
2699 (branch
2700 ByteLiteral
2701 value
2702 .
2703 (constructor
2704 TermApplicationSpine
2705 TermApplicationSpineValue
2706 (constructor Term ByteLiteral value)
2707 (constructor TermList TermListEnd)))
2708 (branch
2709 TermSequenceEnd
2710 .
2711 (constructor
2712 TermApplicationSpine
2713 TermApplicationSpineValue
2714 (constructor Term TermSequenceEnd)
2715 (constructor TermList TermListEnd)))
2716 (branch
2717 TermSequenceNext
2718 head
2719 tail
2720 ih_head
2721 ih_tail
2722 .
2723 (constructor
2724 TermApplicationSpine
2725 TermApplicationSpineValue
2726 (constructor Term TermSequenceNext head tail)
2727 (constructor TermList TermListEnd)))
2728 (branch
2729 TermEliminatorBranch
2730 constructor
2731 binders
2732 body
2733 ih_binders
2734 ih_body
2735 .
2736 (constructor
2737 TermApplicationSpine
2738 TermApplicationSpineValue
2739 (constructor Term TermEliminatorBranch constructor binders body)
2740 (constructor TermList TermListEnd)))
2741 (branch
2742 FamilyApplication
2743 family
2744 arguments
2745 ih_arguments
2746 .
2747 (constructor
2748 TermApplicationSpine
2749 TermApplicationSpineValue
2750 (constructor Term FamilyApplication family arguments)
2751 (constructor TermList TermListEnd)))
2752 (branch
2753 ConstructorApplication
2754 family
2755 constructor
2756 arguments
2757 ih_arguments
2758 .
2759 (constructor
2760 TermApplicationSpine
2761 TermApplicationSpineValue
2762 (constructor Term ConstructorApplication family constructor arguments)
2763 (constructor TermList TermListEnd)))
2764 (branch
2765 Eliminator
2766 family
2767 motive
2768 scrutinee
2769 branches
2770 ih_motive
2771 ih_scrutinee
2772 ih_branches
2773 .
2774 (constructor
2775 TermApplicationSpine
2776 TermApplicationSpineValue
2777 (constructor Term Eliminator family motive scrutinee branches)
2778 (constructor TermList TermListEnd)))
2779 (branch
2780 Match
2781 family
2782 scrutinee
2783 branches
2784 ih_scrutinee
2785 ih_branches
2786 .
2787 (constructor
2788 TermApplicationSpine
2789 TermApplicationSpineValue
2790 (constructor Term Match family scrutinee branches)
2791 (constructor TermList TermListEnd)))
2792 (branch
2793 MatchWith
2794 family
2795 motive
2796 scrutinee
2797 branches
2798 ih_motive
2799 ih_scrutinee
2800 ih_branches
2801 .
2802 (constructor
2803 TermApplicationSpine
2804 TermApplicationSpineValue
2805 (constructor Term MatchWith family motive scrutinee branches)
2806 (constructor TermList TermListEnd)))
2807 (branch
2808 IntegerLiteral
2809 spelling
2810 .
2811 (constructor
2812 TermApplicationSpine
2813 TermApplicationSpineValue
2814 (constructor Term IntegerLiteral spelling)
2815 (constructor TermList TermListEnd)))
2816 (branch
2817 RecordConstruction
2818 name
2819 origin
2820 bindings
2821 ih_bindings
2822 .
2823 (constructor
2824 TermApplicationSpine
2825 TermApplicationSpineValue
2826 (constructor Term RecordConstruction name origin bindings)
2827 (constructor TermList TermListEnd)))
2828 (branch
2829 RecordAssignment
2830 name
2831 origin
2832 value
2833 ih_value
2834 .
2835 (constructor
2836 TermApplicationSpine
2837 TermApplicationSpineValue
2838 (constructor Term RecordAssignment name origin value)
2839 (constructor TermList TermListEnd)))
2840 (branch
2841 RecordProjection
2842 name
2843 field
2844 origin
2845 value
2846 ih_value
2847 .
2848 (constructor
2849 TermApplicationSpine
2850 TermApplicationSpineValue
2851 (constructor Term RecordProjection name field origin value)
2852 (constructor TermList TermListEnd)))
2853 (branch
2854 RecordUpdate
2855 name
2856 origin
2857 value
2858 bindings
2859 ih_value
2860 ih_bindings
2861 .
2862 (constructor
2863 TermApplicationSpine
2864 TermApplicationSpineValue
2865 (constructor Term RecordUpdate name origin value bindings)
2866 (constructor TermList TermListEnd)))
2867 (branch
2868 LocalLet
2869 quantity
2870 binder
2871 hasAnnotation
2872 annotation
2873 value
2874 body
2875 ih_annotation
2876 ih_value
2877 ih_body
2878 .
2879 (constructor
2880 TermApplicationSpine
2881 TermApplicationSpineValue
2882 (constructor Term LocalLet quantity binder hasAnnotation annotation value body)
2883 (constructor TermList TermListEnd)))
2884 (branch
2885 DoBlock
2886 effects
2887 result
2888 body
2889 ih_effects
2890 ih_result
2891 ih_body
2892 .
2893 (constructor
2894 TermApplicationSpine
2895 TermApplicationSpineValue
2896 (constructor Term DoBlock effects result body)
2897 (constructor TermList TermListEnd)))
2898 (branch
2899 DoStep
2900 named
2901 quantity
2902 binder
2903 computation
2904 continuation
2905 ih_computation
2906 ih_continuation
2907 .
2908 (constructor
2909 TermApplicationSpine
2910 TermApplicationSpineValue
2911 (constructor Term DoStep named quantity binder computation continuation)
2912 (constructor TermList TermListEnd)))
2913 (branch
2914 DoReturn
2915 value
2916 ih_value
2917 .
2918 (constructor
2919 TermApplicationSpine
2920 TermApplicationSpineValue
2921 (constructor Term DoReturn value)
2922 (constructor TermList TermListEnd)))))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.