The inspection callback selects only the literal kind admitted by this primitive.
7759def workReduceCorePayloadPair =
7760 (lambda unrestricted inspect : (pi unrestricted term : (family CoreTerm) . (pi unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (pi unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (family CoreWorkResult)))) .
7761 (lambda unrestricted primitive : (family CorePrimitive) .
7762 (lambda unrestricted left : (family CoreTerm) .
7763 (lambda unrestricted right : (family CoreTerm) .
7764 (lambda unrestricted budget : (family NormalizationBudget) .
7765 (app
7766 (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) .
7767 (inspect
7768 left
7769 (lambda unrestricted leftPayload : Bytes .
7770 (inspect
7771 right
7772 (lambda unrestricted rightPayload : Bytes .
7773 (coreWorkChargeBytes
7774 leftPayload
7775 budget
7776 (lambda unrestricted afterLeft : (family NormalizationBudget) .
7777 (coreWorkChargeBytes
7778 rightPayload
7779 afterLeft
7780 (lambda unrestricted afterRight : (family NormalizationBudget) .
7781 (constructor
7782 CoreWorkResult
7783 CoreWorkCompleted
7784 (reduceAppliedCorePrimitive primitive left right)
7785 afterRight))))))
7786 neutral))
7787 neutral))
7788 (lambda unrestricted force : Nat .
7789 (constructor
7790 CoreWorkResult
7791 CoreWorkCompleted
7792 (corePrimitiveApplication2 primitive left right)
7793 budget))))))))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.