4571def decodeHeadWithArgument =
4572 (lambda unrestricted functionTerm : (family Term) .
4573 (lambda unrestricted argumentTerm : (family Term) .
4574 (lambda unrestricted remaining : (family TermList) .
4575 (eliminate
4576 Term
4577 (lambda unrestricted value : (family Term) . (family TermDecodeResult))
4578 functionTerm
4579 (branch
4580 Variable
4581 spelling
4582 .
4583 (decodeVariableHead spelling functionTerm argumentTerm remaining))
4584 (branch Universe level . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4585 (branch NaturalType . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4586 (branch NaturalZero . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4587 (branch
4588 NaturalLiteral
4589 naturalLiteralValue
4590 .
4591 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4592 (branch
4593 NaturalSuccessor
4594 predecessor
4595 ih_predecessor
4596 .
4597 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4598 (branch
4599 Application
4600 function
4601 argument
4602 ih_function
4603 ih_argument
4604 .
4605 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4606 (branch
4607 NaturalArithmetic
4608 operation
4609 function
4610 argument
4611 ih_function
4612 ih_argument
4613 .
4614 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4615 (branch
4616 Lambda
4617 quantityTag
4618 binderSpelling
4619 domain
4620 body
4621 ih_domain
4622 ih_body
4623 .
4624 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4625 (branch
4626 Pi
4627 quantityTag
4628 binderSpelling
4629 domain
4630 codomain
4631 ih_domain
4632 ih_codomain
4633 .
4634 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4635 (branch BytesType . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4636 (branch
4637 BytesLiteral
4638 bytesValue
4639 .
4640 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4641 (branch ByteType . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4642 (branch ByteLiteral byteValue . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4643 (branch TermSequenceEnd . (decodeOrdinaryHead functionTerm argumentTerm remaining))
4644 (branch
4645 TermSequenceNext
4646 sequenceHead
4647 sequenceTail
4648 ih_sequenceHead
4649 ih_sequenceTail
4650 .
4651 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4652 (branch
4653 TermEliminatorBranch
4654 constructorSpelling
4655 binderNames
4656 body
4657 ih_binderNames
4658 ih_body
4659 .
4660 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4661 (branch
4662 FamilyApplication
4663 familySpelling
4664 familyArguments
4665 ih_familyArguments
4666 .
4667 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4668 (branch
4669 ConstructorApplication
4670 familySpelling
4671 constructorSpelling
4672 constructorArguments
4673 ih_constructorArguments
4674 .
4675 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4676 (branch
4677 Eliminator
4678 eliminatedFamilySpelling
4679 motive
4680 scrutinee
4681 branches
4682 ih_motive
4683 ih_scrutinee
4684 ih_branches
4685 .
4686 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4687 (branch
4688 Match
4689 family
4690 scrutinee
4691 branches
4692 ih_scrutinee
4693 ih_branches
4694 .
4695 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4696 (branch
4697 MatchWith
4698 family
4699 motive
4700 scrutinee
4701 branches
4702 ih_motive
4703 ih_scrutinee
4704 ih_branches
4705 .
4706 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4707 (branch
4708 IntegerLiteral
4709 integerLiteralSpelling
4710 .
4711 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4712 (branch
4713 RecordConstruction
4714 name
4715 origin
4716 bindings
4717 ih_bindings
4718 .
4719 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4720 (branch
4721 RecordAssignment
4722 name
4723 origin
4724 value
4725 ih_value
4726 .
4727 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4728 (branch
4729 RecordProjection
4730 name
4731 field
4732 origin
4733 value
4734 ih_value
4735 .
4736 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4737 (branch
4738 RecordUpdate
4739 name
4740 origin
4741 value
4742 bindings
4743 ih_value
4744 ih_bindings
4745 .
4746 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4747 (branch
4748 LocalLet
4749 quantity
4750 binder
4751 hasAnnotation
4752 annotation
4753 value
4754 body
4755 ih_annotation
4756 ih_value
4757 ih_body
4758 .
4759 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4760 (branch
4761 DoBlock
4762 effects
4763 result
4764 body
4765 ih_effects
4766 ih_result
4767 ih_body
4768 .
4769 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4770 (branch
4771 DoStep
4772 named
4773 quantity
4774 binder
4775 computation
4776 continuation
4777 ih_computation
4778 ih_continuation
4779 .
4780 (decodeOrdinaryHead functionTerm argumentTerm remaining))
4781 (branch
4782 DoReturn
4783 value
4784 ih_value
4785 .
4786 (decodeOrdinaryHead functionTerm argumentTerm 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.