1612def naturalValueFromTerm =
1613 (lambda unrestricted term : (family Term) .
1614 (eliminate
1615 Term
1616 (lambda unrestricted value : (family Term) . (family NaturalTermResult))
1617 term
1618 (branch Variable spelling . (constructor NaturalTermResult NotNaturalTerm))
1619 (branch Universe level . (constructor NaturalTermResult NotNaturalTerm))
1620 (branch NaturalType . (constructor NaturalTermResult NotNaturalTerm))
1621 (branch NaturalZero . (constructor NaturalTermResult NaturalTermDecoded zero))
1622 (branch
1623 NaturalLiteral
1624 naturalLiteralValue
1625 .
1626 (constructor NaturalTermResult NaturalTermDecoded naturalLiteralValue))
1627 (branch
1628 NaturalSuccessor
1629 predecessor
1630 ih_predecessor
1631 .
1632 (eliminate
1633 NaturalTermResult
1634 (lambda unrestricted result : (family NaturalTermResult) . (family NaturalTermResult))
1635 ih_predecessor
1636 (branch
1637 NaturalTermDecoded
1638 naturalTermValue
1639 .
1640 (constructor NaturalTermResult NaturalTermDecoded (succ naturalTermValue)))
1641 (branch NotNaturalTerm . (constructor NaturalTermResult NotNaturalTerm))))
1642 (branch
1643 Application
1644 function
1645 argument
1646 ih_function
1647 ih_argument
1648 .
1649 (constructor NaturalTermResult NotNaturalTerm))
1650 (branch
1651 NaturalArithmetic
1652 operation
1653 function
1654 argument
1655 ih_function
1656 ih_argument
1657 .
1658 (constructor NaturalTermResult NotNaturalTerm))
1659 (branch
1660 Lambda
1661 quantityTag
1662 binderSpelling
1663 domain
1664 body
1665 ih_domain
1666 ih_body
1667 .
1668 (constructor NaturalTermResult NotNaturalTerm))
1669 (branch
1670 Pi
1671 quantityTag
1672 binderSpelling
1673 domain
1674 codomain
1675 ih_domain
1676 ih_codomain
1677 .
1678 (constructor NaturalTermResult NotNaturalTerm))
1679 (branch BytesType . (constructor NaturalTermResult NotNaturalTerm))
1680 (branch BytesLiteral bytesValue . (constructor NaturalTermResult NotNaturalTerm))
1681 (branch ByteType . (constructor NaturalTermResult NotNaturalTerm))
1682 (branch ByteLiteral byteValue . (constructor NaturalTermResult NotNaturalTerm))
1683 (branch TermSequenceEnd . (constructor NaturalTermResult NotNaturalTerm))
1684 (branch
1685 TermSequenceNext
1686 sequenceHead
1687 sequenceTail
1688 ih_sequenceHead
1689 ih_sequenceTail
1690 .
1691 (constructor NaturalTermResult NotNaturalTerm))
1692 (branch
1693 TermEliminatorBranch
1694 constructorSpelling
1695 binderNames
1696 body
1697 ih_binderNames
1698 ih_body
1699 .
1700 (constructor NaturalTermResult NotNaturalTerm))
1701 (branch
1702 FamilyApplication
1703 familySpelling
1704 familyArguments
1705 ih_familyArguments
1706 .
1707 (constructor NaturalTermResult NotNaturalTerm))
1708 (branch
1709 ConstructorApplication
1710 familySpelling
1711 constructorSpelling
1712 constructorArguments
1713 ih_constructorArguments
1714 .
1715 (constructor NaturalTermResult NotNaturalTerm))
1716 (branch
1717 Eliminator
1718 eliminatedFamilySpelling
1719 motive
1720 scrutinee
1721 branches
1722 ih_motive
1723 ih_scrutinee
1724 ih_branches
1725 .
1726 (constructor NaturalTermResult NotNaturalTerm))
1727 (branch
1728 Match
1729 family
1730 scrutinee
1731 branches
1732 ih_scrutinee
1733 ih_branches
1734 .
1735 (constructor NaturalTermResult NotNaturalTerm))
1736 (branch
1737 MatchWith
1738 family
1739 motive
1740 scrutinee
1741 branches
1742 ih_motive
1743 ih_scrutinee
1744 ih_branches
1745 .
1746 (constructor NaturalTermResult NotNaturalTerm))
1747 (branch
1748 IntegerLiteral
1749 integerLiteralSpelling
1750 .
1751 (eliminate
1752 DecimalParseResult
1753 (lambda unrestricted result : (family DecimalParseResult) . (family NaturalTermResult))
1754 (parseDecimalSpelling integerLiteralSpelling)
1755 (branch DecimalParsed value . (constructor NaturalTermResult NaturalTermDecoded value))
1756 (branch DecimalInvalid . (constructor NaturalTermResult NotNaturalTerm))))
1757 (branch
1758 RecordConstruction
1759 name
1760 origin
1761 bindings
1762 ih_bindings
1763 .
1764 (constructor NaturalTermResult NotNaturalTerm))
1765 (branch
1766 RecordAssignment
1767 name
1768 origin
1769 value
1770 ih_value
1771 .
1772 (constructor NaturalTermResult NotNaturalTerm))
1773 (branch
1774 RecordProjection
1775 name
1776 field
1777 origin
1778 value
1779 ih_value
1780 .
1781 (constructor NaturalTermResult NotNaturalTerm))
1782 (branch
1783 RecordUpdate
1784 name
1785 origin
1786 value
1787 bindings
1788 ih_value
1789 ih_bindings
1790 .
1791 (constructor NaturalTermResult NotNaturalTerm))
1792 (branch
1793 LocalLet
1794 quantity
1795 binder
1796 hasAnnotation
1797 annotation
1798 value
1799 body
1800 ih_annotation
1801 ih_value
1802 ih_body
1803 .
1804 (constructor NaturalTermResult NotNaturalTerm))
1805 (branch
1806 DoBlock
1807 effects
1808 result
1809 body
1810 ih_effects
1811 ih_result
1812 ih_body
1813 .
1814 (constructor NaturalTermResult NotNaturalTerm))
1815 (branch
1816 DoStep
1817 named
1818 quantity
1819 binder
1820 computation
1821 continuation
1822 ih_computation
1823 ih_continuation
1824 .
1825 (constructor NaturalTermResult NotNaturalTerm))
1826 (branch DoReturn value ih_value . (constructor NaturalTermResult NotNaturalTerm))))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.