Compiler.DependentCore

4464def findCoreEliminatorBranch =
4465  (lambda unrestricted constructorName : Bytes .
4466    (lambda unrestricted branches : (family CoreTerm) .
4467      (eliminate
4468        CoreTerm
4469        (lambda unrestricted value : (family CoreTerm) . (family CoreEliminatorBranchSelection))
4470        branches
4471        (branch
4472          CoreUniverse
4473          level
4474          .
4475          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4476        (branch
4477          CoreNatural
4478          .
4479          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4480        (branch
4481          CoreNaturalLiteral
4482          value
4483          .
4484          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4485        (branch
4486          CoreBound
4487          index
4488          .
4489          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4490        (branch
4491          CorePi
4492          multiplicity
4493          domain
4494          codomain
4495          ih_domain
4496          ih_codomain
4497          .
4498          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4499        (branch
4500          CoreLambda
4501          multiplicity
4502          domain
4503          body
4504          ih_domain
4505          ih_body
4506          .
4507          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4508        (branch
4509          CoreLet
4510          multiplicity
4511          annotation
4512          value
4513          body
4514          ih_annotation
4515          ih_value
4516          ih_body
4517          .
4518          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4519        (branch
4520          CoreApplication
4521          function
4522          argument
4523          ih_function
4524          ih_argument
4525          .
4526          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4527        (branch
4528          CoreNaturalArithmetic
4529          operation
4530          function
4531          argument
4532          ih_function
4533          ih_argument
4534          .
4535          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4536        (branch
4537          CoreNaturalSuccessor
4538          predecessor
4539          ih_predecessor
4540          .
4541          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4542        (branch CoreByte . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4543        (branch
4544          CoreByteLiteral
4545          value
4546          .
4547          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4548        (branch CoreBytes . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4549        (branch
4550          CoreBytesLiteral
4551          value
4552          .
4553          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4554        (branch
4555          CorePrimitiveTerm
4556          primitive
4557          .
4558          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4559        (branch
4560          CoreTermSequenceEnd
4561          .
4562          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4563        (branch
4564          CoreTermSequenceNext
4565          head
4566          tail
4567          ih_head
4568          ih_tail
4569          .
4570          (chooseCoreEliminatorBranch ih_head ih_tail))
4571        (branch
4572          CoreFamilyApplication
4573          familyName
4574          arguments
4575          ih_arguments
4576          .
4577          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4578        (branch
4579          CoreConstructorApplication
4580          familyName
4581          nestedConstructorName
4582          arguments
4583          ih_arguments
4584          .
4585          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))
4586        (branch
4587          CoreEliminatorBranch
4588          branchConstructorName
4589          binderCount
4590          body
4591          ih_body
4592          .
4593          (nat-eliminate
4594            (lambda unrestricted matches : Nat . (family CoreEliminatorBranchSelection))
4595            (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)
4596            (lambda unrestricted predecessor : Nat .
4597              (lambda unrestricted induction : (family CoreEliminatorBranchSelection) .
4598                (constructor
4599                  CoreEliminatorBranchSelection
4600                  CoreEliminatorBranchSelected
4601                  binderCount
4602                  body)))
4603            (coreBytesEqual branchConstructorName constructorName)))
4604        (branch
4605          CoreEliminator
4606          familyName
4607          motive
4608          scrutinee
4609          nestedBranches
4610          ih_motive
4611          ih_scrutinee
4612          ih_branches
4613          .
4614          (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)))))