1839def resolveNamedCore :
1840 (pi unrestricted term : (family NamedCoreTerm) .
1841 (pi unrestricted scope : (family NameScope) . (family CoreResolutionResult))) =
1842 (lambda unrestricted term : (family NamedCoreTerm) .
1843 (eliminate
1844 NamedCoreTerm
1845 (lambda unrestricted value : (family NamedCoreTerm) .
1846 (pi unrestricted scope : (family NameScope) . (family CoreResolutionResult)))
1847 term
1848 (branch
1849 NamedCoreUniverse
1850 level
1851 .
1852 (lambda unrestricted scope : (family NameScope) .
1853 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreUniverse level))))
1854 (branch
1855 NamedCoreNatural
1856 .
1857 (lambda unrestricted scope : (family NameScope) .
1858 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreNatural))))
1859 (branch
1860 NamedCoreNaturalLiteral
1861 value
1862 .
1863 (lambda unrestricted scope : (family NameScope) .
1864 (constructor
1865 CoreResolutionResult
1866 CoreResolved
1867 (constructor CoreTerm CoreNaturalLiteral value))))
1868 (branch
1869 NamedCoreVariable
1870 identifier
1871 .
1872 (lambda unrestricted scope : (family NameScope) .
1873 (eliminate
1874 NameLookupResult
1875 (lambda unrestricted result : (family NameLookupResult) . (family CoreResolutionResult))
1876 (lookupName scope identifier)
1877 (branch
1878 NameFound
1879 index
1880 .
1881 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreBound index)))
1882 (branch NameNotFound missingIdentifier . (resolveCorePrimitiveName missingIdentifier)))))
1883 (branch
1884 NamedCorePi
1885 multiplicity
1886 binder
1887 domain
1888 codomain
1889 ih_domain
1890 ih_codomain
1891 .
1892 (lambda unrestricted scope : (family NameScope) .
1893 (combineResolvedPi
1894 multiplicity
1895 (ih_domain scope)
1896 (ih_codomain (constructor NameScope NameScopeBinding binder scope)))))
1897 (branch
1898 NamedCoreLambda
1899 multiplicity
1900 binder
1901 domain
1902 body
1903 ih_domain
1904 ih_body
1905 .
1906 (lambda unrestricted scope : (family NameScope) .
1907 (combineResolvedLambda
1908 multiplicity
1909 (ih_domain scope)
1910 (ih_body (constructor NameScope NameScopeBinding binder scope)))))
1911 (branch
1912 NamedCoreLet
1913 multiplicity
1914 binder
1915 annotation
1916 value
1917 body
1918 ih_annotation
1919 ih_value
1920 ih_body
1921 .
1922 (lambda unrestricted scope : (family NameScope) .
1923 (combineResolvedLet
1924 multiplicity
1925 (ih_annotation scope)
1926 (ih_value scope)
1927 (ih_body (constructor NameScope NameScopeBinding binder scope)))))
1928 (branch
1929 NamedCoreApplication
1930 function
1931 argument
1932 ih_function
1933 ih_argument
1934 .
1935 (lambda unrestricted scope : (family NameScope) .
1936 (combineResolvedApplication (ih_function scope) (ih_argument scope))))
1937 (branch
1938 NamedCoreNaturalArithmetic
1939 operation
1940 function
1941 argument
1942 ih_function
1943 ih_argument
1944 .
1945 (lambda unrestricted scope : (family NameScope) .
1946 (combineResolvedArithmetic operation (ih_function scope) (ih_argument scope))))
1947 (branch
1948 NamedCoreNaturalSuccessor
1949 predecessor
1950 ih_predecessor
1951 .
1952 (lambda unrestricted scope : (family NameScope) .
1953 (combineResolvedNaturalSuccessor (ih_predecessor scope))))
1954 (branch
1955 NamedCoreByte
1956 .
1957 (lambda unrestricted scope : (family NameScope) .
1958 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreByte))))
1959 (branch
1960 NamedCoreByteLiteral
1961 value
1962 .
1963 (lambda unrestricted scope : (family NameScope) .
1964 (constructor
1965 CoreResolutionResult
1966 CoreResolved
1967 (constructor CoreTerm CoreByteLiteral value))))
1968 (branch
1969 NamedCoreBytes
1970 .
1971 (lambda unrestricted scope : (family NameScope) .
1972 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreBytes))))
1973 (branch
1974 NamedCoreBytesLiteral
1975 value
1976 .
1977 (lambda unrestricted scope : (family NameScope) .
1978 (constructor
1979 CoreResolutionResult
1980 CoreResolved
1981 (constructor CoreTerm CoreBytesLiteral value))))
1982 (branch
1983 NamedCoreTermSequenceEnd
1984 .
1985 (lambda unrestricted scope : (family NameScope) .
1986 (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreTermSequenceEnd))))
1987 (branch
1988 NamedCoreTermSequenceNext
1989 head
1990 tail
1991 ih_head
1992 ih_tail
1993 .
1994 (lambda unrestricted scope : (family NameScope) .
1995 (combineResolvedTermSequence (ih_head scope) (ih_tail scope))))
1996 (branch
1997 NamedCoreFamilyApplication
1998 familyName
1999 arguments
2000 ih_arguments
2001 .
2002 (lambda unrestricted scope : (family NameScope) .
2003 (combineResolvedFamilyApplication familyName (ih_arguments scope))))
2004 (branch
2005 NamedCoreConstructorApplication
2006 familyName
2007 constructorName
2008 arguments
2009 ih_arguments
2010 .
2011 (lambda unrestricted scope : (family NameScope) .
2012 (combineResolvedConstructorApplication familyName constructorName (ih_arguments scope))))
2013 (branch
2014 NamedCoreEliminatorBranch
2015 constructorName
2016 binderNames
2017 body
2018 ih_binderNames
2019 ih_body
2020 .
2021 (lambda unrestricted scope : (family NameScope) .
2022 (finishResolvedEliminatorBranchScope
2023 constructorName
2024 ih_body
2025 (resolveEliminatorBranchScope binderNames scope))))
2026 (branch
2027 NamedCoreEliminator
2028 familyName
2029 motive
2030 scrutinee
2031 branches
2032 ih_motive
2033 ih_scrutinee
2034 ih_branches
2035 .
2036 (lambda unrestricted scope : (family NameScope) .
2037 (combineResolvedEliminator
2038 familyName
2039 (ih_motive scope)
2040 (ih_scrutinee scope)
2041 (ih_branches scope))))))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.