Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 5278–5326

extendCoreFunctionInspection

Full file
5278def extendCoreFunctionInspection :
5279  (pi unrestricted inspection : (family CoreFunctionInspection) .
5280    (pi unrestricted argument : (family CoreTerm) . (family CoreFunctionInspection))) =
5281  (lambda unrestricted inspection : (family CoreFunctionInspection) .
5282    (lambda unrestricted argument : (family CoreTerm) .
5283      (eliminate
5284        CoreFunctionInspection
5285        (lambda unrestricted value : (family CoreFunctionInspection) .
5286          (family CoreFunctionInspection))
5287        inspection
5288        (branch CoreFunctionLambda body . (constructor CoreFunctionInspection CoreFunctionOther))
5289        (branch
5290          CoreFunctionPrimitive
5291          primitive
5292          .
5293          (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive primitive argument))
5294        (branch
5295          CoreFunctionAppliedPrimitive
5296          primitive
5297          first
5298          .
5299          (constructor
5300            CoreFunctionInspection
5301            CoreFunctionAppliedPrimitive2
5302            primitive
5303            first
5304            argument))
5305        (branch
5306          CoreFunctionAppliedPrimitive2
5307          primitive
5308          first
5309          second
5310          .
5311          (constructor
5312            CoreFunctionInspection
5313            CoreFunctionAppliedPrimitive3
5314            primitive
5315            first
5316            second
5317            argument))
5318        (branch
5319          CoreFunctionAppliedPrimitive3
5320          primitive
5321          first
5322          second
5323          third
5324          .
5325          (constructor CoreFunctionInspection CoreFunctionOther))
5326        (branch CoreFunctionOther . (constructor CoreFunctionInspection CoreFunctionOther)))))

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.