1527def resolveEliminatorBranchScope =
1528 (lambda unrestricted binders : (family NamedCoreTerm) .
1529 (eliminate
1530 NamedCoreTerm
1531 (lambda unrestricted value : (family NamedCoreTerm) .
1532 (pi unrestricted scope : (family NameScope) . (family EliminatorBranchScopeResolution)))
1533 binders
1534 (branch
1535 NamedCoreUniverse
1536 level
1537 .
1538 (lambda unrestricted scope : (family NameScope) .
1539 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1540 (branch
1541 NamedCoreNatural
1542 .
1543 (lambda unrestricted scope : (family NameScope) .
1544 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1545 (branch
1546 NamedCoreNaturalLiteral
1547 value
1548 .
1549 (lambda unrestricted scope : (family NameScope) .
1550 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1551 (branch
1552 NamedCoreVariable
1553 identifier
1554 .
1555 (lambda unrestricted scope : (family NameScope) .
1556 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1557 (branch
1558 NamedCorePi
1559 multiplicity
1560 binder
1561 domain
1562 codomain
1563 ih_domain
1564 ih_codomain
1565 .
1566 (lambda unrestricted scope : (family NameScope) .
1567 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1568 (branch
1569 NamedCoreLambda
1570 multiplicity
1571 binder
1572 domain
1573 body
1574 ih_domain
1575 ih_body
1576 .
1577 (lambda unrestricted scope : (family NameScope) .
1578 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1579 (branch
1580 NamedCoreLet
1581 multiplicity
1582 binder
1583 annotation
1584 value
1585 body
1586 ih_annotation
1587 ih_value
1588 ih_body
1589 .
1590 (lambda unrestricted scope : (family NameScope) .
1591 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1592 (branch
1593 NamedCoreApplication
1594 function
1595 argument
1596 ih_function
1597 ih_argument
1598 .
1599 (lambda unrestricted scope : (family NameScope) .
1600 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1601 (branch
1602 NamedCoreNaturalArithmetic
1603 operation
1604 function
1605 argument
1606 ih_function
1607 ih_argument
1608 .
1609 (lambda unrestricted scope : (family NameScope) .
1610 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1611 (branch
1612 NamedCoreNaturalSuccessor
1613 predecessor
1614 ih_predecessor
1615 .
1616 (lambda unrestricted scope : (family NameScope) .
1617 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1618 (branch
1619 NamedCoreByte
1620 .
1621 (lambda unrestricted scope : (family NameScope) .
1622 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1623 (branch
1624 NamedCoreByteLiteral
1625 value
1626 .
1627 (lambda unrestricted scope : (family NameScope) .
1628 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1629 (branch
1630 NamedCoreBytes
1631 .
1632 (lambda unrestricted scope : (family NameScope) .
1633 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1634 (branch
1635 NamedCoreBytesLiteral
1636 value
1637 .
1638 (lambda unrestricted scope : (family NameScope) .
1639 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1640 (branch
1641 NamedCoreTermSequenceEnd
1642 .
1643 (lambda unrestricted scope : (family NameScope) .
1644 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeResolved scope zero)))
1645 (branch
1646 NamedCoreTermSequenceNext
1647 head
1648 tail
1649 ih_head
1650 ih_tail
1651 .
1652 (lambda unrestricted scope : (family NameScope) .
1653 (eliminate
1654 NamedCoreVariableInspection
1655 (lambda unrestricted inspection : (family NamedCoreVariableInspection) .
1656 (family EliminatorBranchScopeResolution))
1657 (inspectNamedCoreVariable head)
1658 (branch
1659 NamedCoreVariableFound
1660 identifier
1661 .
1662 (extendEliminatorBranchScope identifier (ih_tail scope)))
1663 (branch
1664 NamedCoreTermIsNotVariable
1665 .
1666 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))))
1667 (branch
1668 NamedCoreFamilyApplication
1669 familyName
1670 arguments
1671 ih_arguments
1672 .
1673 (lambda unrestricted scope : (family NameScope) .
1674 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1675 (branch
1676 NamedCoreConstructorApplication
1677 familyName
1678 constructorName
1679 arguments
1680 ih_arguments
1681 .
1682 (lambda unrestricted scope : (family NameScope) .
1683 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1684 (branch
1685 NamedCoreEliminatorBranch
1686 constructorName
1687 binderNames
1688 body
1689 ih_binderNames
1690 ih_body
1691 .
1692 (lambda unrestricted scope : (family NameScope) .
1693 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))
1694 (branch
1695 NamedCoreEliminator
1696 familyName
1697 motive
1698 scrutinee
1699 branches
1700 ih_motive
1701 ih_scrutinee
1702 ih_branches
1703 .
1704 (lambda unrestricted scope : (family NameScope) .
1705 (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected)))))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.