9393def workCountCoreTermSequence =
9394 (lambda unrestricted sequence : (family CoreTerm) .
9395 (eliminate
9396 CoreTerm
9397 (lambda unrestricted current : (family CoreTerm) .
9398 (pi unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9399 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))))
9400 sequence
9401 (branch
9402 CoreUniverse
9403 level
9404 .
9405 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9406 (lambda unrestricted budget : (family NormalizationBudget) .
9407 (coreWorkCharge
9408 coreWorkOne
9409 budget
9410 (lambda unrestricted remaining : (family NormalizationBudget) .
9411 (continuation zero remaining))))))
9412 (branch
9413 CoreNatural
9414 .
9415 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9416 (lambda unrestricted budget : (family NormalizationBudget) .
9417 (coreWorkCharge
9418 coreWorkOne
9419 budget
9420 (lambda unrestricted remaining : (family NormalizationBudget) .
9421 (continuation zero remaining))))))
9422 (branch
9423 CoreNaturalLiteral
9424 value
9425 .
9426 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9427 (lambda unrestricted budget : (family NormalizationBudget) .
9428 (coreWorkCharge
9429 coreWorkOne
9430 budget
9431 (lambda unrestricted remaining : (family NormalizationBudget) .
9432 (continuation zero remaining))))))
9433 (branch
9434 CoreBound
9435 index
9436 .
9437 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9438 (lambda unrestricted budget : (family NormalizationBudget) .
9439 (coreWorkCharge
9440 coreWorkOne
9441 budget
9442 (lambda unrestricted remaining : (family NormalizationBudget) .
9443 (continuation zero remaining))))))
9444 (branch
9445 CorePi
9446 multiplicity
9447 domain
9448 codomain
9449 ih_domain
9450 ih_codomain
9451 .
9452 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9453 (lambda unrestricted budget : (family NormalizationBudget) .
9454 (coreWorkCharge
9455 coreWorkOne
9456 budget
9457 (lambda unrestricted remaining : (family NormalizationBudget) .
9458 (continuation zero remaining))))))
9459 (branch
9460 CoreLambda
9461 multiplicity
9462 domain
9463 body
9464 ih_domain
9465 ih_body
9466 .
9467 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9468 (lambda unrestricted budget : (family NormalizationBudget) .
9469 (coreWorkCharge
9470 coreWorkOne
9471 budget
9472 (lambda unrestricted remaining : (family NormalizationBudget) .
9473 (continuation zero remaining))))))
9474 (branch
9475 CoreLet
9476 multiplicity
9477 annotation
9478 value
9479 body
9480 ih_annotation
9481 ih_value
9482 ih_body
9483 .
9484 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9485 (lambda unrestricted budget : (family NormalizationBudget) .
9486 (coreWorkCharge
9487 coreWorkOne
9488 budget
9489 (lambda unrestricted remaining : (family NormalizationBudget) .
9490 (continuation zero remaining))))))
9491 (branch
9492 CoreApplication
9493 function
9494 argument
9495 ih_function
9496 ih_argument
9497 .
9498 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9499 (lambda unrestricted budget : (family NormalizationBudget) .
9500 (coreWorkCharge
9501 coreWorkOne
9502 budget
9503 (lambda unrestricted remaining : (family NormalizationBudget) .
9504 (continuation zero remaining))))))
9505 (branch
9506 CoreNaturalArithmetic
9507 operation
9508 function
9509 argument
9510 ih_function
9511 ih_argument
9512 .
9513 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9514 (lambda unrestricted budget : (family NormalizationBudget) .
9515 (coreWorkCharge
9516 coreWorkOne
9517 budget
9518 (lambda unrestricted remaining : (family NormalizationBudget) .
9519 (continuation zero remaining))))))
9520 (branch
9521 CoreNaturalSuccessor
9522 predecessor
9523 ih_predecessor
9524 .
9525 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9526 (lambda unrestricted budget : (family NormalizationBudget) .
9527 (coreWorkCharge
9528 coreWorkOne
9529 budget
9530 (lambda unrestricted remaining : (family NormalizationBudget) .
9531 (continuation zero remaining))))))
9532 (branch
9533 CoreByte
9534 .
9535 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9536 (lambda unrestricted budget : (family NormalizationBudget) .
9537 (coreWorkCharge
9538 coreWorkOne
9539 budget
9540 (lambda unrestricted remaining : (family NormalizationBudget) .
9541 (continuation zero remaining))))))
9542 (branch
9543 CoreByteLiteral
9544 value
9545 .
9546 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9547 (lambda unrestricted budget : (family NormalizationBudget) .
9548 (coreWorkCharge
9549 coreWorkOne
9550 budget
9551 (lambda unrestricted remaining : (family NormalizationBudget) .
9552 (continuation zero remaining))))))
9553 (branch
9554 CoreBytes
9555 .
9556 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9557 (lambda unrestricted budget : (family NormalizationBudget) .
9558 (coreWorkCharge
9559 coreWorkOne
9560 budget
9561 (lambda unrestricted remaining : (family NormalizationBudget) .
9562 (continuation zero remaining))))))
9563 (branch
9564 CoreBytesLiteral
9565 value
9566 .
9567 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9568 (lambda unrestricted budget : (family NormalizationBudget) .
9569 (coreWorkCharge
9570 coreWorkOne
9571 budget
9572 (lambda unrestricted remaining : (family NormalizationBudget) .
9573 (continuation zero remaining))))))
9574 (branch
9575 CorePrimitiveTerm
9576 primitive
9577 .
9578 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9579 (lambda unrestricted budget : (family NormalizationBudget) .
9580 (coreWorkCharge
9581 coreWorkOne
9582 budget
9583 (lambda unrestricted remaining : (family NormalizationBudget) .
9584 (continuation zero remaining))))))
9585 (branch
9586 CoreTermSequenceEnd
9587 .
9588 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9589 (lambda unrestricted budget : (family NormalizationBudget) .
9590 (coreWorkCharge
9591 coreWorkOne
9592 budget
9593 (lambda unrestricted remaining : (family NormalizationBudget) .
9594 (continuation zero remaining))))))
9595 (branch
9596 CoreTermSequenceNext
9597 head
9598 tail
9599 ih_head
9600 ih_tail
9601 .
9602 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9603 (lambda unrestricted budget : (family NormalizationBudget) .
9604 (coreWorkCharge
9605 coreWorkOne
9606 budget
9607 (lambda unrestricted remaining : (family NormalizationBudget) .
9608 (ih_tail
9609 (lambda unrestricted count : Nat .
9610 (lambda unrestricted afterTail : (family NormalizationBudget) .
9611 (continuation (succ count) afterTail)))
9612 remaining))))))
9613 (branch
9614 CoreFamilyApplication
9615 familyName
9616 arguments
9617 ih_arguments
9618 .
9619 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9620 (lambda unrestricted budget : (family NormalizationBudget) .
9621 (coreWorkCharge
9622 coreWorkOne
9623 budget
9624 (lambda unrestricted remaining : (family NormalizationBudget) .
9625 (continuation zero remaining))))))
9626 (branch
9627 CoreConstructorApplication
9628 familyName
9629 constructorName
9630 arguments
9631 ih_arguments
9632 .
9633 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9634 (lambda unrestricted budget : (family NormalizationBudget) .
9635 (coreWorkCharge
9636 coreWorkOne
9637 budget
9638 (lambda unrestricted remaining : (family NormalizationBudget) .
9639 (continuation zero remaining))))))
9640 (branch
9641 CoreEliminatorBranch
9642 constructorName
9643 binderCount
9644 body
9645 ih_body
9646 .
9647 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9648 (lambda unrestricted budget : (family NormalizationBudget) .
9649 (coreWorkCharge
9650 coreWorkOne
9651 budget
9652 (lambda unrestricted remaining : (family NormalizationBudget) .
9653 (continuation zero remaining))))))
9654 (branch
9655 CoreEliminator
9656 familyName
9657 motive
9658 scrutinee
9659 branches
9660 ih_motive
9661 ih_scrutinee
9662 ih_branches
9663 .
9664 (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) .
9665 (lambda unrestricted budget : (family NormalizationBudget) .
9666 (coreWorkCharge
9667 coreWorkOne
9668 budget
9669 (lambda unrestricted remaining : (family NormalizationBudget) .
9670 (continuation zero remaining))))))))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.