Compiler.DependentCore

2552def reduceCoreTypeApplication :
2553  (pi unrestricted function : (family CoreTerm) .
2554    (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) =
2555  (lambda unrestricted function : (family CoreTerm) .
2556    (eliminate
2557      CoreTerm
2558      (lambda unrestricted value : (family CoreTerm) .
2559        (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)))
2560      function
2561      (branch
2562        CoreUniverse
2563        level
2564        .
2565        (lambda unrestricted argument : (family CoreTerm) .
2566          (constructor CoreTerm CoreApplication function argument)))
2567      (branch
2568        CoreNatural
2569        .
2570        (lambda unrestricted argument : (family CoreTerm) .
2571          (constructor CoreTerm CoreApplication function argument)))
2572      (branch
2573        CoreNaturalLiteral
2574        value
2575        .
2576        (lambda unrestricted argument : (family CoreTerm) .
2577          (constructor CoreTerm CoreApplication function argument)))
2578      (branch
2579        CoreBound
2580        index
2581        .
2582        (lambda unrestricted argument : (family CoreTerm) .
2583          (constructor CoreTerm CoreApplication function argument)))
2584      (branch
2585        CorePi
2586        multiplicity
2587        domain
2588        codomain
2589        ih_domain
2590        ih_codomain
2591        .
2592        (lambda unrestricted argument : (family CoreTerm) .
2593          (constructor CoreTerm CoreApplication function argument)))
2594      (branch
2595        CoreLambda
2596        multiplicity
2597        domain
2598        body
2599        ih_domain
2600        ih_body
2601        .
2602        (lambda unrestricted argument : (family CoreTerm) . (substituteCoreTop argument body)))
2603      (branch
2604        CoreLet
2605        multiplicity
2606        annotation
2607        value
2608        body
2609        ih_annotation
2610        ih_value
2611        ih_body
2612        .
2613        (lambda unrestricted argument : (family CoreTerm) .
2614          (constructor CoreTerm CoreApplication function argument)))
2615      (branch
2616        CoreApplication
2617        nestedFunction
2618        nestedArgument
2619        ih_nestedFunction
2620        ih_nestedArgument
2621        .
2622        (lambda unrestricted argument : (family CoreTerm) .
2623          (constructor CoreTerm CoreApplication function argument)))
2624      (branch
2625        CoreNaturalArithmetic
2626        operation
2627        nestedFunction
2628        nestedArgument
2629        ih_nestedFunction
2630        ih_nestedArgument
2631        .
2632        (lambda unrestricted argument : (family CoreTerm) .
2633          (constructor CoreTerm CoreApplication function argument)))
2634      (branch
2635        CoreNaturalSuccessor
2636        predecessor
2637        ih_predecessor
2638        .
2639        (lambda unrestricted argument : (family CoreTerm) .
2640          (constructor CoreTerm CoreApplication function argument)))
2641      (branch
2642        CoreByte
2643        .
2644        (lambda unrestricted argument : (family CoreTerm) .
2645          (constructor CoreTerm CoreApplication function argument)))
2646      (branch
2647        CoreByteLiteral
2648        value
2649        .
2650        (lambda unrestricted argument : (family CoreTerm) .
2651          (constructor CoreTerm CoreApplication function argument)))
2652      (branch
2653        CoreBytes
2654        .
2655        (lambda unrestricted argument : (family CoreTerm) .
2656          (constructor CoreTerm CoreApplication function argument)))
2657      (branch
2658        CoreBytesLiteral
2659        value
2660        .
2661        (lambda unrestricted argument : (family CoreTerm) .
2662          (constructor CoreTerm CoreApplication function argument)))
2663      (branch
2664        CorePrimitiveTerm
2665        primitive
2666        .
2667        (lambda unrestricted argument : (family CoreTerm) .
2668          (constructor CoreTerm CoreApplication function argument)))
2669      (branch
2670        CoreTermSequenceEnd
2671        .
2672        (lambda unrestricted argument : (family CoreTerm) .
2673          (constructor CoreTerm CoreApplication function argument)))
2674      (branch
2675        CoreTermSequenceNext
2676        head
2677        tail
2678        ih_head
2679        ih_tail
2680        .
2681        (lambda unrestricted argument : (family CoreTerm) .
2682          (constructor CoreTerm CoreApplication function argument)))
2683      (branch
2684        CoreFamilyApplication
2685        familyName
2686        arguments
2687        ih_arguments
2688        .
2689        (lambda unrestricted argument : (family CoreTerm) .
2690          (constructor CoreTerm CoreApplication function argument)))
2691      (branch
2692        CoreConstructorApplication
2693        familyName
2694        constructorName
2695        arguments
2696        ih_arguments
2697        .
2698        (lambda unrestricted argument : (family CoreTerm) .
2699          (constructor CoreTerm CoreApplication function argument)))
2700      (branch
2701        CoreEliminatorBranch
2702        constructorName
2703        binderCount
2704        body
2705        ih_body
2706        .
2707        (lambda unrestricted argument : (family CoreTerm) .
2708          (constructor CoreTerm CoreApplication function argument)))
2709      (branch
2710        CoreEliminator
2711        familyName
2712        motive
2713        scrutinee
2714        branches
2715        ih_motive
2716        ih_scrutinee
2717        ih_branches
2718        .
2719        (lambda unrestricted argument : (family CoreTerm) .
2720          (constructor CoreTerm CoreApplication function argument)))))