Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 12781–12813

reduceCoreApplication

Full file
12781def reduceCoreApplication :
12782  (pi unrestricted function : (family CoreTerm) .
12783    (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) =
12784  (lambda unrestricted function : (family CoreTerm) .
12785    (lambda unrestricted argument : (family CoreTerm) .
12786      (eliminate
12787        CoreFunctionInspection
12788        (lambda unrestricted inspection : (family CoreFunctionInspection) . (family CoreTerm))
12789        (inspectCoreFunction function)
12790        (branch CoreFunctionLambda body . (substituteCoreTop argument body))
12791        (branch CoreFunctionPrimitive primitive . (reduceDirectCorePrimitive primitive argument))
12792        (branch
12793          CoreFunctionAppliedPrimitive
12794          primitive
12795          left
12796          .
12797          (reduceAppliedCorePrimitive primitive left argument))
12798        (branch
12799          CoreFunctionAppliedPrimitive2
12800          primitive
12801          first
12802          second
12803          .
12804          (corePrimitiveApplication3 primitive first second argument))
12805        (branch
12806          CoreFunctionAppliedPrimitive3
12807          primitive
12808          first
12809          second
12810          third
12811          .
12812          (reduceAppliedCoreEliminator primitive first second third argument))
12813        (branch CoreFunctionOther . (constructor CoreTerm CoreApplication function argument)))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.