Compiler.DependentCore

4664def appendCoreTermSequenceForEliminator =
4665  (lambda unrestricted left : (family CoreTerm) .
4666    (eliminate
4667      CoreTerm
4668      (lambda unrestricted value : (family CoreTerm) .
4669        (pi unrestricted right : (family CoreTerm) . (family CoreTerm)))
4670      left
4671      (branch CoreUniverse level . (lambda unrestricted right : (family CoreTerm) . left))
4672      (branch CoreNatural . (lambda unrestricted right : (family CoreTerm) . left))
4673      (branch CoreNaturalLiteral value . (lambda unrestricted right : (family CoreTerm) . left))
4674      (branch CoreBound index . (lambda unrestricted right : (family CoreTerm) . left))
4675      (branch
4676        CorePi
4677        multiplicity
4678        domain
4679        codomain
4680        ih_domain
4681        ih_codomain
4682        .
4683        (lambda unrestricted right : (family CoreTerm) . left))
4684      (branch
4685        CoreLambda
4686        multiplicity
4687        domain
4688        body
4689        ih_domain
4690        ih_body
4691        .
4692        (lambda unrestricted right : (family CoreTerm) . left))
4693      (branch
4694        CoreLet
4695        multiplicity
4696        annotation
4697        value
4698        body
4699        ih_annotation
4700        ih_value
4701        ih_body
4702        .
4703        (lambda unrestricted right : (family CoreTerm) . left))
4704      (branch
4705        CoreApplication
4706        function
4707        argument
4708        ih_function
4709        ih_argument
4710        .
4711        (lambda unrestricted right : (family CoreTerm) . left))
4712      (branch
4713        CoreNaturalArithmetic
4714        operation
4715        function
4716        argument
4717        ih_function
4718        ih_argument
4719        .
4720        (lambda unrestricted right : (family CoreTerm) . left))
4721      (branch
4722        CoreNaturalSuccessor
4723        predecessor
4724        ih_predecessor
4725        .
4726        (lambda unrestricted right : (family CoreTerm) . left))
4727      (branch CoreByte . (lambda unrestricted right : (family CoreTerm) . left))
4728      (branch CoreByteLiteral value . (lambda unrestricted right : (family CoreTerm) . left))
4729      (branch CoreBytes . (lambda unrestricted right : (family CoreTerm) . left))
4730      (branch CoreBytesLiteral value . (lambda unrestricted right : (family CoreTerm) . left))
4731      (branch CorePrimitiveTerm primitive . (lambda unrestricted right : (family CoreTerm) . left))
4732      (branch CoreTermSequenceEnd . (lambda unrestricted right : (family CoreTerm) . right))
4733      (branch
4734        CoreTermSequenceNext
4735        head
4736        tail
4737        ih_head
4738        ih_tail
4739        .
4740        (lambda unrestricted right : (family CoreTerm) .
4741          (constructor CoreTerm CoreTermSequenceNext head (ih_tail right))))
4742      (branch
4743        CoreFamilyApplication
4744        familyName
4745        arguments
4746        ih_arguments
4747        .
4748        (lambda unrestricted right : (family CoreTerm) . left))
4749      (branch
4750        CoreConstructorApplication
4751        familyName
4752        constructorName
4753        arguments
4754        ih_arguments
4755        .
4756        (lambda unrestricted right : (family CoreTerm) . left))
4757      (branch
4758        CoreEliminatorBranch
4759        constructorName
4760        binderCount
4761        body
4762        ih_body
4763        .
4764        (lambda unrestricted right : (family CoreTerm) . left))
4765      (branch
4766        CoreEliminator
4767        familyName
4768        motive
4769        scrutinee
4770        branches
4771        ih_motive
4772        ih_scrutinee
4773        ih_branches
4774        .
4775        (lambda unrestricted right : (family CoreTerm) . left))))