Compiler.DependentCore

4278def coreTermEqual :
4279  (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . Nat)) =
4280  (lambda unrestricted left : (family CoreTerm) .
4281    (eliminate
4282      CoreTerm
4283      (lambda unrestricted term : (family CoreTerm) .
4284        (pi unrestricted right : (family CoreTerm) . Nat))
4285      left
4286      (branch CoreUniverse level . (coreUniverseEqual level))
4287      (branch CoreNatural . coreNaturalEqual)
4288      (branch CoreNaturalLiteral value . (coreNaturalLiteralEqual value))
4289      (branch CoreBound index . (coreBoundEqual index))
4290      (branch
4291        CorePi
4292        multiplicity
4293        domain
4294        codomain
4295        ih_domain
4296        ih_codomain
4297        .
4298        (corePiEqual multiplicity ih_domain ih_codomain))
4299      (branch
4300        CoreLambda
4301        multiplicity
4302        domain
4303        body
4304        ih_domain
4305        ih_body
4306        .
4307        (coreLambdaEqual multiplicity ih_domain ih_body))
4308      (branch
4309        CoreLet
4310        multiplicity
4311        annotation
4312        value
4313        body
4314        ih_annotation
4315        ih_value
4316        ih_body
4317        .
4318        (coreLetEqual multiplicity ih_annotation ih_value ih_body))
4319      (branch
4320        CoreApplication
4321        function
4322        argument
4323        ih_function
4324        ih_argument
4325        .
4326        (coreApplicationEqual ih_function ih_argument))
4327      (branch
4328        CoreNaturalArithmetic
4329        operation
4330        function
4331        argument
4332        ih_function
4333        ih_argument
4334        .
4335        (coreArithmeticEqual operation ih_function ih_argument))
4336      (branch
4337        CoreNaturalSuccessor
4338        predecessor
4339        ih_predecessor
4340        .
4341        (coreNaturalSuccessorEqual ih_predecessor))
4342      (branch CoreByte . coreByteEqual)
4343      (branch CoreByteLiteral value . (coreByteLiteralEqual value))
4344      (branch CoreBytes . coreBytesTypeEqual)
4345      (branch CoreBytesLiteral value . (coreBytesLiteralEqual value))
4346      (branch CorePrimitiveTerm primitive . (corePrimitiveTermEqual primitive))
4347      (branch CoreTermSequenceEnd . coreTermSequenceEndEqual)
4348      (branch
4349        CoreTermSequenceNext
4350        head
4351        tail
4352        ih_head
4353        ih_tail
4354        .
4355        (coreTermSequenceNextEqual ih_head ih_tail))
4356      (branch
4357        CoreFamilyApplication
4358        familyName
4359        arguments
4360        ih_arguments
4361        .
4362        (coreFamilyApplicationEqual familyName ih_arguments))
4363      (branch
4364        CoreConstructorApplication
4365        familyName
4366        constructorName
4367        arguments
4368        ih_arguments
4369        .
4370        (coreConstructorApplicationEqual familyName constructorName ih_arguments))
4371      (branch
4372        CoreEliminatorBranch
4373        constructorName
4374        binderCount
4375        body
4376        ih_body
4377        .
4378        (coreEliminatorBranchEqual constructorName binderCount ih_body))
4379      (branch
4380        CoreEliminator
4381        familyName
4382        motive
4383        scrutinee
4384        branches
4385        ih_motive
4386        ih_scrutinee
4387        ih_branches
4388        .
4389        (coreEliminatorEqual familyName ih_motive ih_scrutinee ih_branches))))