Compiler.DependentCore

2722def inspectCoreLiteral :
2723  (pi unrestricted term : (family CoreTerm) . (family CoreLiteralInspection)) =
2724  (lambda unrestricted term : (family CoreTerm) .
2725    (eliminate
2726      CoreTerm
2727      (lambda unrestricted value : (family CoreTerm) . (family CoreLiteralInspection))
2728      term
2729      (branch CoreUniverse level . (constructor CoreLiteralInspection CoreNotLiteral))
2730      (branch CoreNatural . (constructor CoreLiteralInspection CoreNotLiteral))
2731      (branch
2732        CoreNaturalLiteral
2733        value
2734        .
2735        (constructor CoreLiteralInspection CoreNaturalInspected value))
2736      (branch CoreBound index . (constructor CoreLiteralInspection CoreNotLiteral))
2737      (branch
2738        CorePi
2739        multiplicity
2740        domain
2741        codomain
2742        ih_domain
2743        ih_codomain
2744        .
2745        (constructor CoreLiteralInspection CoreNotLiteral))
2746      (branch
2747        CoreLambda
2748        multiplicity
2749        domain
2750        body
2751        ih_domain
2752        ih_body
2753        .
2754        (constructor CoreLiteralInspection CoreNotLiteral))
2755      (branch
2756        CoreLet
2757        multiplicity
2758        annotation
2759        value
2760        body
2761        ih_annotation
2762        ih_value
2763        ih_body
2764        .
2765        (constructor CoreLiteralInspection CoreNotLiteral))
2766      (branch
2767        CoreApplication
2768        function
2769        argument
2770        ih_function
2771        ih_argument
2772        .
2773        (constructor CoreLiteralInspection CoreNotLiteral))
2774      (branch
2775        CoreNaturalArithmetic
2776        operation
2777        function
2778        argument
2779        ih_function
2780        ih_argument
2781        .
2782        (constructor CoreLiteralInspection CoreNotLiteral))
2783      (branch
2784        CoreNaturalSuccessor
2785        predecessor
2786        ih_predecessor
2787        .
2788        (constructor CoreLiteralInspection CoreNotLiteral))
2789      (branch CoreByte . (constructor CoreLiteralInspection CoreNotLiteral))
2790      (branch CoreByteLiteral value . (constructor CoreLiteralInspection CoreByteInspected value))
2791      (branch CoreBytes . (constructor CoreLiteralInspection CoreNotLiteral))
2792      (branch CoreBytesLiteral value . (constructor CoreLiteralInspection CoreBytesInspected value))
2793      (branch CorePrimitiveTerm primitive . (constructor CoreLiteralInspection CoreNotLiteral))
2794      (branch CoreTermSequenceEnd . (constructor CoreLiteralInspection CoreNotLiteral))
2795      (branch
2796        CoreTermSequenceNext
2797        head
2798        tail
2799        ih_head
2800        ih_tail
2801        .
2802        (constructor CoreLiteralInspection CoreNotLiteral))
2803      (branch
2804        CoreFamilyApplication
2805        familyName
2806        arguments
2807        ih_arguments
2808        .
2809        (constructor CoreLiteralInspection CoreNotLiteral))
2810      (branch
2811        CoreConstructorApplication
2812        familyName
2813        constructorName
2814        arguments
2815        ih_arguments
2816        .
2817        (constructor CoreLiteralInspection CoreNotLiteral))
2818      (branch
2819        CoreEliminatorBranch
2820        constructorName
2821        binderCount
2822        body
2823        ih_body
2824        .
2825        (constructor CoreLiteralInspection CoreNotLiteral))
2826      (branch
2827        CoreEliminator
2828        familyName
2829        motive
2830        scrutinee
2831        branches
2832        ih_motive
2833        ih_scrutinee
2834        ih_branches
2835        .
2836        (constructor CoreLiteralInspection CoreNotLiteral))))