8429def workReduceBytesEliminator =
8430 (lambda unrestricted motive : (family CoreTerm) .
8431 (lambda unrestricted emptyCase : (family CoreTerm) .
8432 (lambda unrestricted consCase : (family CoreTerm) .
8433 (lambda unrestricted scrutinee : (family CoreTerm) .
8434 (lambda unrestricted budget : (family NormalizationBudget) .
8435 (workInspectCoreBytes
8436 scrutinee
8437 (lambda unrestricted payload : Bytes .
8438 (coreWorkChargeBytes
8439 payload
8440 budget
8441 (lambda unrestricted remaining : (family NormalizationBudget) .
8442 (app
8443 (bytes-eliminate
8444 (lambda unrestricted current : Bytes .
8445 (pi unrestricted allowance : (family NormalizationBudget) .
8446 (family CoreWorkResult)))
8447 (lambda unrestricted allowance : (family NormalizationBudget) .
8448 (constructor CoreWorkResult CoreWorkCompleted emptyCase allowance))
8449 (lambda unrestricted head : Byte .
8450 (lambda unrestricted tail : Bytes .
8451 (lambda unrestricted induction : (pi unrestricted allowance : (family NormalizationBudget) . (family CoreWorkResult)) .
8452 (lambda unrestricted allowance : (family NormalizationBudget) .
8453 (coreWorkBind
8454 (induction allowance)
8455 (lambda unrestricted value : (family CoreTerm) .
8456 (lambda unrestricted afterInduction : (family NormalizationBudget) .
8457 (workReduceBytesEliminateStep
8458 consCase
8459 head
8460 tail
8461 value
8462 afterInduction))))))))
8463 payload)
8464 remaining))))
8465 (lambda unrestricted force : Nat .
8466 (constructor
8467 CoreWorkResult
8468 CoreWorkCompleted
8469 (corePrimitiveApplication4
8470 (constructor CorePrimitive CoreBytesEliminate)
8471 motive
8472 emptyCase
8473 consCase
8474 scrutinee)
8475 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.