Compiler.DependentCore

12815def betaReduceOne : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) =
12816  (lambda unrestricted term : (family CoreTerm) .
12817    (eliminate
12818      CoreTerm
12819      (lambda unrestricted value : (family CoreTerm) . (family CoreTerm))
12820      term
12821      (branch CoreUniverse level . (constructor CoreTerm CoreUniverse level))
12822      (branch CoreNatural . (constructor CoreTerm CoreNatural))
12823      (branch CoreNaturalLiteral value . (constructor CoreTerm CoreNaturalLiteral value))
12824      (branch CoreBound index . (constructor CoreTerm CoreBound index))
12825      (branch
12826        CorePi
12827        multiplicity
12828        domain
12829        codomain
12830        ih_domain
12831        ih_codomain
12832        .
12833        (constructor CoreTerm CorePi multiplicity ih_domain ih_codomain))
12834      (branch
12835        CoreLambda
12836        multiplicity
12837        domain
12838        body
12839        ih_domain
12840        ih_body
12841        .
12842        (constructor CoreTerm CoreLambda multiplicity ih_domain ih_body))
12843      (branch
12844        CoreLet
12845        multiplicity
12846        annotation
12847        value
12848        body
12849        ih_annotation
12850        ih_value
12851        ih_body
12852        .
12853        (substituteCoreTop ih_value ih_body))
12854      (branch
12855        CoreApplication
12856        function
12857        argument
12858        ih_function
12859        ih_argument
12860        .
12861        (reduceCoreApplication ih_function ih_argument))
12862      (branch
12863        CoreNaturalArithmetic
12864        operation
12865        function
12866        argument
12867        ih_function
12868        ih_argument
12869        .
12870        (reduceCoreArithmetic operation ih_function ih_argument))
12871      (branch
12872        CoreNaturalSuccessor
12873        predecessor
12874        ih_predecessor
12875        .
12876        (reduceCoreNaturalSuccessor ih_predecessor))
12877      (branch CoreByte . (constructor CoreTerm CoreByte))
12878      (branch CoreByteLiteral value . (constructor CoreTerm CoreByteLiteral value))
12879      (branch CoreBytes . (constructor CoreTerm CoreBytes))
12880      (branch CoreBytesLiteral value . (constructor CoreTerm CoreBytesLiteral value))
12881      (branch CorePrimitiveTerm primitive . (constructor CoreTerm CorePrimitiveTerm primitive))
12882      (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd))
12883      (branch
12884        CoreTermSequenceNext
12885        head
12886        tail
12887        ih_head
12888        ih_tail
12889        .
12890        (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail))
12891      (branch
12892        CoreFamilyApplication
12893        familyName
12894        arguments
12895        ih_arguments
12896        .
12897        (constructor CoreTerm CoreFamilyApplication familyName ih_arguments))
12898      (branch
12899        CoreConstructorApplication
12900        familyName
12901        constructorName
12902        arguments
12903        ih_arguments
12904        .
12905        (constructor CoreTerm CoreConstructorApplication familyName constructorName ih_arguments))
12906      (branch
12907        CoreEliminatorBranch
12908        constructorName
12909        binderCount
12910        body
12911        ih_body
12912        .
12913        (constructor CoreTerm CoreEliminatorBranch constructorName binderCount ih_body))
12914      (branch
12915        CoreEliminator
12916        familyName
12917        motive
12918        scrutinee
12919        branches
12920        ih_motive
12921        ih_scrutinee
12922        ih_branches
12923        .
12924        (reduceCoreGenericEliminator familyName ih_motive ih_scrutinee ih_branches))))