7819def workReduceCoreBytesCons =
7820 (lambda unrestricted left : (family CoreTerm) .
7821 (lambda unrestricted right : (family CoreTerm) .
7822 (lambda unrestricted budget : (family NormalizationBudget) .
7823 (app
7824 (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) .
7825 (workInspectCoreByte
7826 left
7827 (lambda unrestricted head : Byte .
7828 (workInspectCoreBytes
7829 right
7830 (lambda unrestricted tail : Bytes .
7831 (coreWorkCharge
7832 coreWorkOne
7833 budget
7834 (lambda unrestricted afterHead : (family NormalizationBudget) .
7835 (coreWorkChargeBytes
7836 tail
7837 afterHead
7838 (lambda unrestricted remaining : (family NormalizationBudget) .
7839 (constructor
7840 CoreWorkResult
7841 CoreWorkCompleted
7842 (reduceCoreBytesCons left right)
7843 remaining))))))
7844 neutral))
7845 neutral))
7846 (lambda unrestricted force : Nat .
7847 (constructor
7848 CoreWorkResult
7849 CoreWorkCompleted
7850 (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)
7851 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.