Compiler.DependentCore

4777def instantiateCoreEliminatorBranch =
4778  (lambda unrestricted supplied : (family CoreTerm) .
4779    (eliminate
4780      CoreTerm
4781      (lambda unrestricted value : (family CoreTerm) .
4782        (pi unrestricted body : (family CoreTerm) . (family CoreTerm)))
4783      supplied
4784      (branch CoreUniverse level . (lambda unrestricted body : (family CoreTerm) . body))
4785      (branch CoreNatural . (lambda unrestricted body : (family CoreTerm) . body))
4786      (branch CoreNaturalLiteral value . (lambda unrestricted body : (family CoreTerm) . body))
4787      (branch CoreBound index . (lambda unrestricted body : (family CoreTerm) . body))
4788      (branch
4789        CorePi
4790        multiplicity
4791        domain
4792        codomain
4793        ih_domain
4794        ih_codomain
4795        .
4796        (lambda unrestricted body : (family CoreTerm) . body))
4797      (branch
4798        CoreLambda
4799        multiplicity
4800        domain
4801        body
4802        ih_domain
4803        ih_body
4804        .
4805        (lambda unrestricted branchBody : (family CoreTerm) . branchBody))
4806      (branch
4807        CoreLet
4808        multiplicity
4809        annotation
4810        value
4811        body
4812        ih_annotation
4813        ih_value
4814        ih_body
4815        .
4816        (lambda unrestricted branchBody : (family CoreTerm) . branchBody))
4817      (branch
4818        CoreApplication
4819        function
4820        argument
4821        ih_function
4822        ih_argument
4823        .
4824        (lambda unrestricted body : (family CoreTerm) . body))
4825      (branch
4826        CoreNaturalArithmetic
4827        operation
4828        function
4829        argument
4830        ih_function
4831        ih_argument
4832        .
4833        (lambda unrestricted body : (family CoreTerm) . body))
4834      (branch
4835        CoreNaturalSuccessor
4836        predecessor
4837        ih_predecessor
4838        .
4839        (lambda unrestricted body : (family CoreTerm) . body))
4840      (branch CoreByte . (lambda unrestricted body : (family CoreTerm) . body))
4841      (branch CoreByteLiteral value . (lambda unrestricted body : (family CoreTerm) . body))
4842      (branch CoreBytes . (lambda unrestricted body : (family CoreTerm) . body))
4843      (branch CoreBytesLiteral value . (lambda unrestricted body : (family CoreTerm) . body))
4844      (branch CorePrimitiveTerm primitive . (lambda unrestricted body : (family CoreTerm) . body))
4845      (branch CoreTermSequenceEnd . (lambda unrestricted body : (family CoreTerm) . body))
4846      (branch
4847        CoreTermSequenceNext
4848        head
4849        tail
4850        ih_head
4851        ih_tail
4852        .
4853        (lambda unrestricted body : (family CoreTerm) . (substituteCoreTop head (ih_tail body))))
4854      (branch
4855        CoreFamilyApplication
4856        familyName
4857        arguments
4858        ih_arguments
4859        .
4860        (lambda unrestricted body : (family CoreTerm) . body))
4861      (branch
4862        CoreConstructorApplication
4863        familyName
4864        constructorName
4865        arguments
4866        ih_arguments
4867        .
4868        (lambda unrestricted body : (family CoreTerm) . body))
4869      (branch
4870        CoreEliminatorBranch
4871        constructorName
4872        binderCount
4873        body
4874        ih_body
4875        .
4876        (lambda unrestricted branchBody : (family CoreTerm) . branchBody))
4877      (branch
4878        CoreEliminator
4879        familyName
4880        motive
4881        scrutinee
4882        branches
4883        ih_motive
4884        ih_scrutinee
4885        ih_branches
4886        .
4887        (lambda unrestricted body : (family CoreTerm) . body))))