9114def workInstantiateCoreEliminatorBranch =
9115 (lambda unrestricted supplied : (family CoreTerm) .
9116 (eliminate
9117 CoreTerm
9118 (lambda unrestricted value : (family CoreTerm) .
9119 (pi unrestricted body : (family CoreTerm) .
9120 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))))
9121 supplied
9122 (branch
9123 CoreUniverse
9124 level
9125 .
9126 (lambda unrestricted body : (family CoreTerm) .
9127 (lambda unrestricted budget : (family NormalizationBudget) .
9128 (coreWorkCharge
9129 coreWorkOne
9130 budget
9131 (lambda unrestricted remaining : (family NormalizationBudget) .
9132 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9133 (branch
9134 CoreNatural
9135 .
9136 (lambda unrestricted body : (family CoreTerm) .
9137 (lambda unrestricted budget : (family NormalizationBudget) .
9138 (coreWorkCharge
9139 coreWorkOne
9140 budget
9141 (lambda unrestricted remaining : (family NormalizationBudget) .
9142 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9143 (branch
9144 CoreNaturalLiteral
9145 value
9146 .
9147 (lambda unrestricted body : (family CoreTerm) .
9148 (lambda unrestricted budget : (family NormalizationBudget) .
9149 (coreWorkCharge
9150 coreWorkOne
9151 budget
9152 (lambda unrestricted remaining : (family NormalizationBudget) .
9153 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9154 (branch
9155 CoreBound
9156 index
9157 .
9158 (lambda unrestricted body : (family CoreTerm) .
9159 (lambda unrestricted budget : (family NormalizationBudget) .
9160 (coreWorkCharge
9161 coreWorkOne
9162 budget
9163 (lambda unrestricted remaining : (family NormalizationBudget) .
9164 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9165 (branch
9166 CorePi
9167 multiplicity
9168 domain
9169 codomain
9170 ih_domain
9171 ih_codomain
9172 .
9173 (lambda unrestricted body : (family CoreTerm) .
9174 (lambda unrestricted budget : (family NormalizationBudget) .
9175 (coreWorkCharge
9176 coreWorkOne
9177 budget
9178 (lambda unrestricted remaining : (family NormalizationBudget) .
9179 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9180 (branch
9181 CoreLambda
9182 multiplicity
9183 domain
9184 body
9185 ih_domain
9186 ih_body
9187 .
9188 (lambda unrestricted branchBody : (family CoreTerm) .
9189 (lambda unrestricted budget : (family NormalizationBudget) .
9190 (coreWorkCharge
9191 coreWorkOne
9192 budget
9193 (lambda unrestricted remaining : (family NormalizationBudget) .
9194 (constructor CoreWorkResult CoreWorkCompleted branchBody remaining))))))
9195 (branch
9196 CoreLet
9197 multiplicity
9198 annotation
9199 value
9200 body
9201 ih_annotation
9202 ih_value
9203 ih_body
9204 .
9205 (lambda unrestricted branchBody : (family CoreTerm) .
9206 (lambda unrestricted budget : (family NormalizationBudget) .
9207 (coreWorkCharge
9208 coreWorkOne
9209 budget
9210 (lambda unrestricted remaining : (family NormalizationBudget) .
9211 (constructor CoreWorkResult CoreWorkCompleted branchBody remaining))))))
9212 (branch
9213 CoreApplication
9214 function
9215 argument
9216 ih_function
9217 ih_argument
9218 .
9219 (lambda unrestricted body : (family CoreTerm) .
9220 (lambda unrestricted budget : (family NormalizationBudget) .
9221 (coreWorkCharge
9222 coreWorkOne
9223 budget
9224 (lambda unrestricted remaining : (family NormalizationBudget) .
9225 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9226 (branch
9227 CoreNaturalArithmetic
9228 operation
9229 function
9230 argument
9231 ih_function
9232 ih_argument
9233 .
9234 (lambda unrestricted body : (family CoreTerm) .
9235 (lambda unrestricted budget : (family NormalizationBudget) .
9236 (coreWorkCharge
9237 coreWorkOne
9238 budget
9239 (lambda unrestricted remaining : (family NormalizationBudget) .
9240 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9241 (branch
9242 CoreNaturalSuccessor
9243 predecessor
9244 ih_predecessor
9245 .
9246 (lambda unrestricted body : (family CoreTerm) .
9247 (lambda unrestricted budget : (family NormalizationBudget) .
9248 (coreWorkCharge
9249 coreWorkOne
9250 budget
9251 (lambda unrestricted remaining : (family NormalizationBudget) .
9252 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9253 (branch
9254 CoreByte
9255 .
9256 (lambda unrestricted body : (family CoreTerm) .
9257 (lambda unrestricted budget : (family NormalizationBudget) .
9258 (coreWorkCharge
9259 coreWorkOne
9260 budget
9261 (lambda unrestricted remaining : (family NormalizationBudget) .
9262 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9263 (branch
9264 CoreByteLiteral
9265 value
9266 .
9267 (lambda unrestricted body : (family CoreTerm) .
9268 (lambda unrestricted budget : (family NormalizationBudget) .
9269 (coreWorkCharge
9270 coreWorkOne
9271 budget
9272 (lambda unrestricted remaining : (family NormalizationBudget) .
9273 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9274 (branch
9275 CoreBytes
9276 .
9277 (lambda unrestricted body : (family CoreTerm) .
9278 (lambda unrestricted budget : (family NormalizationBudget) .
9279 (coreWorkCharge
9280 coreWorkOne
9281 budget
9282 (lambda unrestricted remaining : (family NormalizationBudget) .
9283 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9284 (branch
9285 CoreBytesLiteral
9286 value
9287 .
9288 (lambda unrestricted body : (family CoreTerm) .
9289 (lambda unrestricted budget : (family NormalizationBudget) .
9290 (coreWorkCharge
9291 coreWorkOne
9292 budget
9293 (lambda unrestricted remaining : (family NormalizationBudget) .
9294 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9295 (branch
9296 CorePrimitiveTerm
9297 primitive
9298 .
9299 (lambda unrestricted body : (family CoreTerm) .
9300 (lambda unrestricted budget : (family NormalizationBudget) .
9301 (coreWorkCharge
9302 coreWorkOne
9303 budget
9304 (lambda unrestricted remaining : (family NormalizationBudget) .
9305 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9306 (branch
9307 CoreTermSequenceEnd
9308 .
9309 (lambda unrestricted body : (family CoreTerm) .
9310 (lambda unrestricted budget : (family NormalizationBudget) .
9311 (coreWorkCharge
9312 coreWorkOne
9313 budget
9314 (lambda unrestricted remaining : (family NormalizationBudget) .
9315 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9316 (branch
9317 CoreTermSequenceNext
9318 head
9319 tail
9320 ih_head
9321 ih_tail
9322 .
9323 (lambda unrestricted body : (family CoreTerm) .
9324 (lambda unrestricted budget : (family NormalizationBudget) .
9325 (coreWorkCharge
9326 coreWorkOne
9327 budget
9328 (lambda unrestricted remaining : (family NormalizationBudget) .
9329 (coreWorkBind
9330 (ih_tail body remaining)
9331 (lambda unrestricted afterTail : (family CoreTerm) .
9332 (lambda unrestricted afterTailBudget : (family NormalizationBudget) .
9333 (workSubstituteCoreTop head afterTail afterTailBudget)))))))))
9334 (branch
9335 CoreFamilyApplication
9336 familyName
9337 arguments
9338 ih_arguments
9339 .
9340 (lambda unrestricted body : (family CoreTerm) .
9341 (lambda unrestricted budget : (family NormalizationBudget) .
9342 (coreWorkCharge
9343 coreWorkOne
9344 budget
9345 (lambda unrestricted remaining : (family NormalizationBudget) .
9346 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9347 (branch
9348 CoreConstructorApplication
9349 familyName
9350 constructorName
9351 arguments
9352 ih_arguments
9353 .
9354 (lambda unrestricted body : (family CoreTerm) .
9355 (lambda unrestricted budget : (family NormalizationBudget) .
9356 (coreWorkCharge
9357 coreWorkOne
9358 budget
9359 (lambda unrestricted remaining : (family NormalizationBudget) .
9360 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))
9361 (branch
9362 CoreEliminatorBranch
9363 constructorName
9364 binderCount
9365 body
9366 ih_body
9367 .
9368 (lambda unrestricted branchBody : (family CoreTerm) .
9369 (lambda unrestricted budget : (family NormalizationBudget) .
9370 (coreWorkCharge
9371 coreWorkOne
9372 budget
9373 (lambda unrestricted remaining : (family NormalizationBudget) .
9374 (constructor CoreWorkResult CoreWorkCompleted branchBody remaining))))))
9375 (branch
9376 CoreEliminator
9377 familyName
9378 motive
9379 scrutinee
9380 branches
9381 ih_motive
9382 ih_scrutinee
9383 ih_branches
9384 .
9385 (lambda unrestricted body : (family CoreTerm) .
9386 (lambda unrestricted budget : (family NormalizationBudget) .
9387 (coreWorkCharge
9388 coreWorkOne
9389 budget
9390 (lambda unrestricted remaining : (family NormalizationBudget) .
9391 (constructor CoreWorkResult CoreWorkCompleted body remaining))))))))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.