1707def finishResolvedEliminatorBranch =
1708 (lambda unrestricted constructorName : Bytes .
1709 (lambda unrestricted binderCount : Nat .
1710 (lambda unrestricted bodyResult : (family CoreResolutionResult) .
1711 (eliminate
1712 CoreResolutionResult
1713 (lambda unrestricted value : (family CoreResolutionResult) .
1714 (family CoreResolutionResult))
1715 bodyResult
1716 (branch
1717 CoreResolved
1718 body
1719 .
1720 (constructor
1721 CoreResolutionResult
1722 CoreResolved
1723 (constructor CoreTerm CoreEliminatorBranch constructorName binderCount body)))
1724 (branch
1725 CoreResolutionFailed
1726 identifier
1727 .
1728 (constructor CoreResolutionResult CoreResolutionFailed identifier))))))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.