2062def shiftCore :
2063 (pi unrestricted term : (family CoreTerm) .
2064 (pi unrestricted cutoff : Nat . (pi unrestricted amount : Nat . (family CoreTerm)))) =
2065 (lambda unrestricted term : (family CoreTerm) .
2066 (eliminate
2067 CoreTerm
2068 (lambda unrestricted value : (family CoreTerm) .
2069 (pi unrestricted cutoff : Nat . (pi unrestricted amount : Nat . (family CoreTerm))))
2070 term
2071 (branch
2072 CoreUniverse
2073 level
2074 .
2075 (lambda unrestricted cutoff : Nat .
2076 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreUniverse level))))
2077 (branch
2078 CoreNatural
2079 .
2080 (lambda unrestricted cutoff : Nat .
2081 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNatural))))
2082 (branch
2083 CoreNaturalLiteral
2084 value
2085 .
2086 (lambda unrestricted cutoff : Nat .
2087 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNaturalLiteral value))))
2088 (branch CoreBound index . (shiftCorePart1 index))
2089 (branch
2090 CorePi
2091 multiplicity
2092 domain
2093 codomain
2094 ih_domain
2095 ih_codomain
2096 .
2097 (lambda unrestricted cutoff : Nat .
2098 (lambda unrestricted amount : Nat .
2099 (constructor
2100 CoreTerm
2101 CorePi
2102 multiplicity
2103 (ih_domain cutoff amount)
2104 (ih_codomain (succ cutoff) amount)))))
2105 (branch
2106 CoreLambda
2107 multiplicity
2108 domain
2109 body
2110 ih_domain
2111 ih_body
2112 .
2113 (lambda unrestricted cutoff : Nat .
2114 (lambda unrestricted amount : Nat .
2115 (constructor
2116 CoreTerm
2117 CoreLambda
2118 multiplicity
2119 (ih_domain cutoff amount)
2120 (ih_body (succ cutoff) amount)))))
2121 (branch
2122 CoreLet
2123 multiplicity
2124 annotation
2125 value
2126 body
2127 ih_annotation
2128 ih_value
2129 ih_body
2130 .
2131 (lambda unrestricted cutoff : Nat .
2132 (lambda unrestricted amount : Nat .
2133 (constructor
2134 CoreTerm
2135 CoreLet
2136 multiplicity
2137 (ih_annotation cutoff amount)
2138 (ih_value cutoff amount)
2139 (ih_body (succ cutoff) amount)))))
2140 (branch
2141 CoreApplication
2142 function
2143 argument
2144 ih_function
2145 ih_argument
2146 .
2147 (lambda unrestricted cutoff : Nat .
2148 (lambda unrestricted amount : Nat .
2149 (constructor
2150 CoreTerm
2151 CoreApplication
2152 (ih_function cutoff amount)
2153 (ih_argument cutoff amount)))))
2154 (branch
2155 CoreNaturalArithmetic
2156 operation
2157 function
2158 argument
2159 ih_function
2160 ih_argument
2161 .
2162 (lambda unrestricted cutoff : Nat .
2163 (lambda unrestricted amount : Nat .
2164 (constructor
2165 CoreTerm
2166 CoreNaturalArithmetic
2167 operation
2168 (ih_function cutoff amount)
2169 (ih_argument cutoff amount)))))
2170 (branch
2171 CoreNaturalSuccessor
2172 predecessor
2173 ih_predecessor
2174 .
2175 (lambda unrestricted cutoff : Nat .
2176 (lambda unrestricted amount : Nat .
2177 (constructor CoreTerm CoreNaturalSuccessor (ih_predecessor cutoff amount)))))
2178 (branch
2179 CoreByte
2180 .
2181 (lambda unrestricted cutoff : Nat .
2182 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreByte))))
2183 (branch
2184 CoreByteLiteral
2185 value
2186 .
2187 (lambda unrestricted cutoff : Nat .
2188 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreByteLiteral value))))
2189 (branch
2190 CoreBytes
2191 .
2192 (lambda unrestricted cutoff : Nat .
2193 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreBytes))))
2194 (branch
2195 CoreBytesLiteral
2196 value
2197 .
2198 (lambda unrestricted cutoff : Nat .
2199 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreBytesLiteral value))))
2200 (branch
2201 CorePrimitiveTerm
2202 primitive
2203 .
2204 (lambda unrestricted cutoff : Nat .
2205 (lambda unrestricted amount : Nat . (constructor CoreTerm CorePrimitiveTerm primitive))))
2206 (branch
2207 CoreTermSequenceEnd
2208 .
2209 (lambda unrestricted cutoff : Nat .
2210 (lambda unrestricted amount : Nat . (constructor CoreTerm CoreTermSequenceEnd))))
2211 (branch
2212 CoreTermSequenceNext
2213 head
2214 tail
2215 ih_head
2216 ih_tail
2217 .
2218 (lambda unrestricted cutoff : Nat .
2219 (lambda unrestricted amount : Nat .
2220 (constructor
2221 CoreTerm
2222 CoreTermSequenceNext
2223 (ih_head cutoff amount)
2224 (ih_tail cutoff amount)))))
2225 (branch
2226 CoreFamilyApplication
2227 familyName
2228 arguments
2229 ih_arguments
2230 .
2231 (lambda unrestricted cutoff : Nat .
2232 (lambda unrestricted amount : Nat .
2233 (constructor CoreTerm CoreFamilyApplication familyName (ih_arguments cutoff amount)))))
2234 (branch
2235 CoreConstructorApplication
2236 familyName
2237 constructorName
2238 arguments
2239 ih_arguments
2240 .
2241 (lambda unrestricted cutoff : Nat .
2242 (lambda unrestricted amount : Nat .
2243 (constructor
2244 CoreTerm
2245 CoreConstructorApplication
2246 familyName
2247 constructorName
2248 (ih_arguments cutoff amount)))))
2249 (branch
2250 CoreEliminatorBranch
2251 constructorName
2252 binderCount
2253 body
2254 ih_body
2255 .
2256 (lambda unrestricted cutoff : Nat .
2257 (lambda unrestricted amount : Nat .
2258 (constructor
2259 CoreTerm
2260 CoreEliminatorBranch
2261 constructorName
2262 binderCount
2263 (ih_body (naturalAdd cutoff binderCount) amount)))))
2264 (branch
2265 CoreEliminator
2266 familyName
2267 motive
2268 scrutinee
2269 branches
2270 ih_motive
2271 ih_scrutinee
2272 ih_branches
2273 .
2274 (lambda unrestricted cutoff : Nat .
2275 (lambda unrestricted amount : Nat .
2276 (constructor
2277 CoreTerm
2278 CoreEliminator
2279 familyName
2280 (ih_motive cutoff amount)
2281 (ih_scrutinee cutoff amount)
2282 (ih_branches cutoff amount)))))))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.