Compiler.DependentCore

4889def dropCoreTermSequenceForEliminator =
4890  (lambda unrestricted sequence : (family CoreTerm) .
4891    (eliminate
4892      CoreTerm
4893      (lambda unrestricted value : (family CoreTerm) .
4894        (pi unrestricted count : Nat . (family CoreTerm)))
4895      sequence
4896      (branch CoreUniverse level . (lambda unrestricted count : Nat . sequence))
4897      (branch CoreNatural . (lambda unrestricted count : Nat . sequence))
4898      (branch CoreNaturalLiteral value . (lambda unrestricted count : Nat . sequence))
4899      (branch CoreBound index . (lambda unrestricted count : Nat . sequence))
4900      (branch
4901        CorePi
4902        multiplicity
4903        domain
4904        codomain
4905        ih_domain
4906        ih_codomain
4907        .
4908        (lambda unrestricted count : Nat . sequence))
4909      (branch
4910        CoreLambda
4911        multiplicity
4912        domain
4913        body
4914        ih_domain
4915        ih_body
4916        .
4917        (lambda unrestricted count : Nat . sequence))
4918      (branch
4919        CoreLet
4920        multiplicity
4921        annotation
4922        value
4923        body
4924        ih_annotation
4925        ih_value
4926        ih_body
4927        .
4928        (lambda unrestricted count : Nat . sequence))
4929      (branch
4930        CoreApplication
4931        function
4932        argument
4933        ih_function
4934        ih_argument
4935        .
4936        (lambda unrestricted count : Nat . sequence))
4937      (branch
4938        CoreNaturalArithmetic
4939        operation
4940        function
4941        argument
4942        ih_function
4943        ih_argument
4944        .
4945        (lambda unrestricted count : Nat . sequence))
4946      (branch
4947        CoreNaturalSuccessor
4948        predecessor
4949        ih_predecessor
4950        .
4951        (lambda unrestricted count : Nat . sequence))
4952      (branch CoreByte . (lambda unrestricted count : Nat . sequence))
4953      (branch CoreByteLiteral value . (lambda unrestricted count : Nat . sequence))
4954      (branch CoreBytes . (lambda unrestricted count : Nat . sequence))
4955      (branch CoreBytesLiteral value . (lambda unrestricted count : Nat . sequence))
4956      (branch CorePrimitiveTerm primitive . (lambda unrestricted count : Nat . sequence))
4957      (branch
4958        CoreTermSequenceEnd
4959        .
4960        (lambda unrestricted count : Nat . (constructor CoreTerm CoreTermSequenceEnd)))
4961      (branch
4962        CoreTermSequenceNext
4963        head
4964        tail
4965        ih_head
4966        ih_tail
4967        .
4968        (lambda unrestricted count : Nat .
4969          (nat-eliminate
4970            (lambda unrestricted remaining : Nat . (family CoreTerm))
4971            (constructor CoreTerm CoreTermSequenceNext head tail)
4972            (lambda unrestricted predecessor : Nat .
4973              (lambda unrestricted induction : (family CoreTerm) . (ih_tail predecessor)))
4974            count)))
4975      (branch
4976        CoreFamilyApplication
4977        familyName
4978        arguments
4979        ih_arguments
4980        .
4981        (lambda unrestricted count : Nat . sequence))
4982      (branch
4983        CoreConstructorApplication
4984        familyName
4985        constructorName
4986        arguments
4987        ih_arguments
4988        .
4989        (lambda unrestricted count : Nat . sequence))
4990      (branch
4991        CoreEliminatorBranch
4992        constructorName
4993        binderCount
4994        body
4995        ih_body
4996        .
4997        (lambda unrestricted count : Nat . sequence))
4998      (branch
4999        CoreEliminator
5000        familyName
5001        motive
5002        scrutinee
5003        branches
5004        ih_motive
5005        ih_scrutinee
5006        ih_branches
5007        .
5008        (lambda unrestricted count : Nat . sequence))))