6013def workSubstituteCoreTree =
6014 (lambda unrestricted term : (family CoreTerm) .
6015 (eliminate
6016 CoreTerm
6017 (lambda unrestricted current : (family CoreTerm) .
6018 (pi unrestricted depth : Nat .
6019 (pi unrestricted replacement : (family CoreTerm) .
6020 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))))
6021 term
6022 (branch
6023 CoreUniverse
6024 coreUniverseLevel
6025 .
6026 (lambda unrestricted depth : Nat .
6027 (lambda unrestricted replacement : (family CoreTerm) .
6028 (lambda unrestricted budget : (family NormalizationBudget) .
6029 (coreWorkCharge
6030 coreWorkOne
6031 budget
6032 (lambda unrestricted remaining : (family NormalizationBudget) .
6033 (constructor
6034 CoreWorkResult
6035 CoreWorkCompleted
6036 (constructor CoreTerm CoreUniverse coreUniverseLevel)
6037 remaining)))))))
6038 (branch
6039 CoreNatural
6040 .
6041 (lambda unrestricted depth : Nat .
6042 (lambda unrestricted replacement : (family CoreTerm) .
6043 (lambda unrestricted budget : (family NormalizationBudget) .
6044 (coreWorkCharge
6045 coreWorkOne
6046 budget
6047 (lambda unrestricted remaining : (family NormalizationBudget) .
6048 (constructor
6049 CoreWorkResult
6050 CoreWorkCompleted
6051 (constructor CoreTerm CoreNatural)
6052 remaining)))))))
6053 (branch
6054 CoreNaturalLiteral
6055 coreNaturalValue
6056 .
6057 (lambda unrestricted depth : Nat .
6058 (lambda unrestricted replacement : (family CoreTerm) .
6059 (lambda unrestricted budget : (family NormalizationBudget) .
6060 (coreWorkCharge
6061 coreWorkOne
6062 budget
6063 (lambda unrestricted remaining : (family NormalizationBudget) .
6064 (constructor
6065 CoreWorkResult
6066 CoreWorkCompleted
6067 (constructor CoreTerm CoreNaturalLiteral coreNaturalValue)
6068 remaining)))))))
6069 (branch
6070 CoreBound
6071 coreBoundIndex
6072 .
6073 (lambda unrestricted depth : Nat .
6074 (lambda unrestricted replacement : (family CoreTerm) .
6075 (lambda unrestricted budget : (family NormalizationBudget) .
6076 (coreWorkCharge
6077 coreWorkOne
6078 budget
6079 (lambda unrestricted remaining : (family NormalizationBudget) .
6080 (coreWorkChoose
6081 (naturalEqual coreBoundIndex depth)
6082 (lambda unrestricted force : Nat .
6083 (workShiftCore replacement zero depth remaining))
6084 (lambda unrestricted force : Nat .
6085 (coreWorkChoose
6086 (nat-less-than depth coreBoundIndex)
6087 (lambda unrestricted force : Nat .
6088 (coreWorkChargeNatural
6089 coreBoundIndex
6090 remaining
6091 (lambda unrestricted remaining : (family NormalizationBudget) .
6092 (constructor
6093 CoreWorkResult
6094 CoreWorkCompleted
6095 (substituteCorePart1 coreBoundIndex depth replacement)
6096 remaining))))
6097 (lambda unrestricted force : Nat .
6098 (constructor
6099 CoreWorkResult
6100 CoreWorkCompleted
6101 (constructor CoreTerm CoreBound coreBoundIndex)
6102 remaining)))))))))))
6103 (branch
6104 CorePi
6105 corePiMultiplicity
6106 corePiDomain
6107 corePiCodomain
6108 ih_corePiDomain
6109 ih_corePiCodomain
6110 .
6111 (lambda unrestricted depth : Nat .
6112 (lambda unrestricted replacement : (family CoreTerm) .
6113 (lambda unrestricted budget : (family NormalizationBudget) .
6114 (coreWorkCharge
6115 coreWorkOne
6116 budget
6117 (lambda unrestricted remaining : (family NormalizationBudget) .
6118 (coreWorkBind
6119 (ih_corePiDomain depth replacement remaining)
6120 (lambda unrestricted new_corePiDomain : (family CoreTerm) .
6121 (lambda unrestricted remaining : (family NormalizationBudget) .
6122 (coreWorkBind
6123 (ih_corePiCodomain (succ depth) replacement remaining)
6124 (lambda unrestricted new_corePiCodomain : (family CoreTerm) .
6125 (lambda unrestricted remaining : (family NormalizationBudget) .
6126 (constructor
6127 CoreWorkResult
6128 CoreWorkCompleted
6129 (constructor
6130 CoreTerm
6131 CorePi
6132 corePiMultiplicity
6133 new_corePiDomain
6134 new_corePiCodomain)
6135 remaining)))))))))))))
6136 (branch
6137 CoreLambda
6138 coreLambdaMultiplicity
6139 coreLambdaDomain
6140 coreLambdaBody
6141 ih_coreLambdaDomain
6142 ih_coreLambdaBody
6143 .
6144 (lambda unrestricted depth : Nat .
6145 (lambda unrestricted replacement : (family CoreTerm) .
6146 (lambda unrestricted budget : (family NormalizationBudget) .
6147 (coreWorkCharge
6148 coreWorkOne
6149 budget
6150 (lambda unrestricted remaining : (family NormalizationBudget) .
6151 (coreWorkBind
6152 (ih_coreLambdaDomain depth replacement remaining)
6153 (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) .
6154 (lambda unrestricted remaining : (family NormalizationBudget) .
6155 (coreWorkBind
6156 (ih_coreLambdaBody (succ depth) replacement remaining)
6157 (lambda unrestricted new_coreLambdaBody : (family CoreTerm) .
6158 (lambda unrestricted remaining : (family NormalizationBudget) .
6159 (constructor
6160 CoreWorkResult
6161 CoreWorkCompleted
6162 (constructor
6163 CoreTerm
6164 CoreLambda
6165 coreLambdaMultiplicity
6166 new_coreLambdaDomain
6167 new_coreLambdaBody)
6168 remaining)))))))))))))
6169 (branch
6170 CoreLet
6171 coreLetMultiplicity
6172 coreLetAnnotation
6173 coreLetValue
6174 coreLetBody
6175 ih_coreLetAnnotation
6176 ih_coreLetValue
6177 ih_coreLetBody
6178 .
6179 (lambda unrestricted depth : Nat .
6180 (lambda unrestricted replacement : (family CoreTerm) .
6181 (lambda unrestricted budget : (family NormalizationBudget) .
6182 (coreWorkCharge
6183 coreWorkOne
6184 budget
6185 (lambda unrestricted remaining : (family NormalizationBudget) .
6186 (coreWorkBind
6187 (ih_coreLetAnnotation depth replacement remaining)
6188 (lambda unrestricted new_coreLetAnnotation : (family CoreTerm) .
6189 (lambda unrestricted remaining : (family NormalizationBudget) .
6190 (coreWorkBind
6191 (ih_coreLetValue depth replacement remaining)
6192 (lambda unrestricted new_coreLetValue : (family CoreTerm) .
6193 (lambda unrestricted remaining : (family NormalizationBudget) .
6194 (coreWorkBind
6195 (ih_coreLetBody (succ depth) replacement remaining)
6196 (lambda unrestricted new_coreLetBody : (family CoreTerm) .
6197 (lambda unrestricted remaining : (family NormalizationBudget) .
6198 (constructor
6199 CoreWorkResult
6200 CoreWorkCompleted
6201 (constructor
6202 CoreTerm
6203 CoreLet
6204 coreLetMultiplicity
6205 new_coreLetAnnotation
6206 new_coreLetValue
6207 new_coreLetBody)
6208 remaining))))))))))))))))
6209 (branch
6210 CoreApplication
6211 coreApplicationFunction
6212 coreApplicationArgument
6213 ih_coreApplicationFunction
6214 ih_coreApplicationArgument
6215 .
6216 (lambda unrestricted depth : Nat .
6217 (lambda unrestricted replacement : (family CoreTerm) .
6218 (lambda unrestricted budget : (family NormalizationBudget) .
6219 (coreWorkCharge
6220 coreWorkOne
6221 budget
6222 (lambda unrestricted remaining : (family NormalizationBudget) .
6223 (coreWorkBind
6224 (ih_coreApplicationFunction depth replacement remaining)
6225 (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) .
6226 (lambda unrestricted remaining : (family NormalizationBudget) .
6227 (coreWorkBind
6228 (ih_coreApplicationArgument depth replacement remaining)
6229 (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) .
6230 (lambda unrestricted remaining : (family NormalizationBudget) .
6231 (constructor
6232 CoreWorkResult
6233 CoreWorkCompleted
6234 (constructor
6235 CoreTerm
6236 CoreApplication
6237 new_coreApplicationFunction
6238 new_coreApplicationArgument)
6239 remaining)))))))))))))
6240 (branch
6241 CoreNaturalArithmetic
6242 coreArithmeticOperation
6243 coreArithmeticLeft
6244 coreArithmeticRight
6245 ih_coreArithmeticLeft
6246 ih_coreArithmeticRight
6247 .
6248 (lambda unrestricted depth : Nat .
6249 (lambda unrestricted replacement : (family CoreTerm) .
6250 (lambda unrestricted budget : (family NormalizationBudget) .
6251 (coreWorkCharge
6252 coreWorkOne
6253 budget
6254 (lambda unrestricted remaining : (family NormalizationBudget) .
6255 (coreWorkBind
6256 (ih_coreArithmeticLeft depth replacement remaining)
6257 (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) .
6258 (lambda unrestricted remaining : (family NormalizationBudget) .
6259 (coreWorkBind
6260 (ih_coreArithmeticRight depth replacement remaining)
6261 (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) .
6262 (lambda unrestricted remaining : (family NormalizationBudget) .
6263 (constructor
6264 CoreWorkResult
6265 CoreWorkCompleted
6266 (constructor
6267 CoreTerm
6268 CoreNaturalArithmetic
6269 coreArithmeticOperation
6270 new_coreArithmeticLeft
6271 new_coreArithmeticRight)
6272 remaining)))))))))))))
6273 (branch
6274 CoreNaturalSuccessor
6275 coreNaturalPredecessor
6276 ih_coreNaturalPredecessor
6277 .
6278 (lambda unrestricted depth : Nat .
6279 (lambda unrestricted replacement : (family CoreTerm) .
6280 (lambda unrestricted budget : (family NormalizationBudget) .
6281 (coreWorkCharge
6282 coreWorkOne
6283 budget
6284 (lambda unrestricted remaining : (family NormalizationBudget) .
6285 (coreWorkBind
6286 (ih_coreNaturalPredecessor depth replacement remaining)
6287 (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) .
6288 (lambda unrestricted remaining : (family NormalizationBudget) .
6289 (constructor
6290 CoreWorkResult
6291 CoreWorkCompleted
6292 (constructor CoreTerm CoreNaturalSuccessor new_coreNaturalPredecessor)
6293 remaining))))))))))
6294 (branch
6295 CoreByte
6296 .
6297 (lambda unrestricted depth : Nat .
6298 (lambda unrestricted replacement : (family CoreTerm) .
6299 (lambda unrestricted budget : (family NormalizationBudget) .
6300 (coreWorkCharge
6301 coreWorkOne
6302 budget
6303 (lambda unrestricted remaining : (family NormalizationBudget) .
6304 (constructor
6305 CoreWorkResult
6306 CoreWorkCompleted
6307 (constructor CoreTerm CoreByte)
6308 remaining)))))))
6309 (branch
6310 CoreByteLiteral
6311 coreByteValue
6312 .
6313 (lambda unrestricted depth : Nat .
6314 (lambda unrestricted replacement : (family CoreTerm) .
6315 (lambda unrestricted budget : (family NormalizationBudget) .
6316 (coreWorkCharge
6317 coreWorkOne
6318 budget
6319 (lambda unrestricted remaining : (family NormalizationBudget) .
6320 (constructor
6321 CoreWorkResult
6322 CoreWorkCompleted
6323 (constructor CoreTerm CoreByteLiteral coreByteValue)
6324 remaining)))))))
6325 (branch
6326 CoreBytes
6327 .
6328 (lambda unrestricted depth : Nat .
6329 (lambda unrestricted replacement : (family CoreTerm) .
6330 (lambda unrestricted budget : (family NormalizationBudget) .
6331 (coreWorkCharge
6332 coreWorkOne
6333 budget
6334 (lambda unrestricted remaining : (family NormalizationBudget) .
6335 (constructor
6336 CoreWorkResult
6337 CoreWorkCompleted
6338 (constructor CoreTerm CoreBytes)
6339 remaining)))))))
6340 (branch
6341 CoreBytesLiteral
6342 coreBytesValue
6343 .
6344 (lambda unrestricted depth : Nat .
6345 (lambda unrestricted replacement : (family CoreTerm) .
6346 (lambda unrestricted budget : (family NormalizationBudget) .
6347 (coreWorkCharge
6348 coreWorkOne
6349 budget
6350 (lambda unrestricted remaining : (family NormalizationBudget) .
6351 (constructor
6352 CoreWorkResult
6353 CoreWorkCompleted
6354 (constructor CoreTerm CoreBytesLiteral coreBytesValue)
6355 remaining)))))))
6356 (branch
6357 CorePrimitiveTerm
6358 corePrimitive
6359 .
6360 (lambda unrestricted depth : Nat .
6361 (lambda unrestricted replacement : (family CoreTerm) .
6362 (lambda unrestricted budget : (family NormalizationBudget) .
6363 (coreWorkCharge
6364 coreWorkOne
6365 budget
6366 (lambda unrestricted remaining : (family NormalizationBudget) .
6367 (constructor
6368 CoreWorkResult
6369 CoreWorkCompleted
6370 (constructor CoreTerm CorePrimitiveTerm corePrimitive)
6371 remaining)))))))
6372 (branch
6373 CoreTermSequenceEnd
6374 .
6375 (lambda unrestricted depth : Nat .
6376 (lambda unrestricted replacement : (family CoreTerm) .
6377 (lambda unrestricted budget : (family NormalizationBudget) .
6378 (coreWorkCharge
6379 coreWorkOne
6380 budget
6381 (lambda unrestricted remaining : (family NormalizationBudget) .
6382 (constructor
6383 CoreWorkResult
6384 CoreWorkCompleted
6385 (constructor CoreTerm CoreTermSequenceEnd)
6386 remaining)))))))
6387 (branch
6388 CoreTermSequenceNext
6389 coreTermSequenceHead
6390 coreTermSequenceTail
6391 ih_coreTermSequenceHead
6392 ih_coreTermSequenceTail
6393 .
6394 (lambda unrestricted depth : Nat .
6395 (lambda unrestricted replacement : (family CoreTerm) .
6396 (lambda unrestricted budget : (family NormalizationBudget) .
6397 (coreWorkCharge
6398 coreWorkOne
6399 budget
6400 (lambda unrestricted remaining : (family NormalizationBudget) .
6401 (coreWorkBind
6402 (ih_coreTermSequenceHead depth replacement remaining)
6403 (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) .
6404 (lambda unrestricted remaining : (family NormalizationBudget) .
6405 (coreWorkBind
6406 (ih_coreTermSequenceTail depth replacement remaining)
6407 (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) .
6408 (lambda unrestricted remaining : (family NormalizationBudget) .
6409 (constructor
6410 CoreWorkResult
6411 CoreWorkCompleted
6412 (constructor
6413 CoreTerm
6414 CoreTermSequenceNext
6415 new_coreTermSequenceHead
6416 new_coreTermSequenceTail)
6417 remaining)))))))))))))
6418 (branch
6419 CoreFamilyApplication
6420 coreFamilyName
6421 coreFamilyArguments
6422 ih_coreFamilyArguments
6423 .
6424 (lambda unrestricted depth : Nat .
6425 (lambda unrestricted replacement : (family CoreTerm) .
6426 (lambda unrestricted budget : (family NormalizationBudget) .
6427 (coreWorkCharge
6428 coreWorkOne
6429 budget
6430 (lambda unrestricted remaining : (family NormalizationBudget) .
6431 (coreWorkBind
6432 (ih_coreFamilyArguments depth replacement remaining)
6433 (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) .
6434 (lambda unrestricted remaining : (family NormalizationBudget) .
6435 (constructor
6436 CoreWorkResult
6437 CoreWorkCompleted
6438 (constructor
6439 CoreTerm
6440 CoreFamilyApplication
6441 coreFamilyName
6442 new_coreFamilyArguments)
6443 remaining))))))))))
6444 (branch
6445 CoreConstructorApplication
6446 coreConstructorFamilyName
6447 coreConstructorName
6448 coreConstructorArguments
6449 ih_coreConstructorArguments
6450 .
6451 (lambda unrestricted depth : Nat .
6452 (lambda unrestricted replacement : (family CoreTerm) .
6453 (lambda unrestricted budget : (family NormalizationBudget) .
6454 (coreWorkCharge
6455 coreWorkOne
6456 budget
6457 (lambda unrestricted remaining : (family NormalizationBudget) .
6458 (coreWorkBind
6459 (ih_coreConstructorArguments depth replacement remaining)
6460 (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) .
6461 (lambda unrestricted remaining : (family NormalizationBudget) .
6462 (constructor
6463 CoreWorkResult
6464 CoreWorkCompleted
6465 (constructor
6466 CoreTerm
6467 CoreConstructorApplication
6468 coreConstructorFamilyName
6469 coreConstructorName
6470 new_coreConstructorArguments)
6471 remaining))))))))))
6472 (branch
6473 CoreEliminatorBranch
6474 coreBranchConstructorName
6475 coreBranchBinderCount
6476 coreBranchBody
6477 ih_coreBranchBody
6478 .
6479 (lambda unrestricted depth : Nat .
6480 (lambda unrestricted replacement : (family CoreTerm) .
6481 (lambda unrestricted budget : (family NormalizationBudget) .
6482 (coreWorkCharge
6483 coreWorkOne
6484 budget
6485 (lambda unrestricted remaining : (family NormalizationBudget) .
6486 (coreWorkChargeNatural
6487 depth
6488 remaining
6489 (lambda unrestricted remaining : (family NormalizationBudget) .
6490 (coreWorkBind
6491 (ih_coreBranchBody
6492 (naturalAdd depth coreBranchBinderCount)
6493 replacement
6494 remaining)
6495 (lambda unrestricted new_coreBranchBody : (family CoreTerm) .
6496 (lambda unrestricted remaining : (family NormalizationBudget) .
6497 (constructor
6498 CoreWorkResult
6499 CoreWorkCompleted
6500 (constructor
6501 CoreTerm
6502 CoreEliminatorBranch
6503 coreBranchConstructorName
6504 coreBranchBinderCount
6505 new_coreBranchBody)
6506 remaining))))))))))))
6507 (branch
6508 CoreEliminator
6509 coreEliminatedFamilyName
6510 coreEliminatorMotive
6511 coreEliminatorScrutinee
6512 coreEliminatorBranches
6513 ih_coreEliminatorMotive
6514 ih_coreEliminatorScrutinee
6515 ih_coreEliminatorBranches
6516 .
6517 (lambda unrestricted depth : Nat .
6518 (lambda unrestricted replacement : (family CoreTerm) .
6519 (lambda unrestricted budget : (family NormalizationBudget) .
6520 (coreWorkCharge
6521 coreWorkOne
6522 budget
6523 (lambda unrestricted remaining : (family NormalizationBudget) .
6524 (coreWorkBind
6525 (ih_coreEliminatorMotive depth replacement remaining)
6526 (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) .
6527 (lambda unrestricted remaining : (family NormalizationBudget) .
6528 (coreWorkBind
6529 (ih_coreEliminatorScrutinee depth replacement remaining)
6530 (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) .
6531 (lambda unrestricted remaining : (family NormalizationBudget) .
6532 (coreWorkBind
6533 (ih_coreEliminatorBranches depth replacement remaining)
6534 (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) .
6535 (lambda unrestricted remaining : (family NormalizationBudget) .
6536 (constructor
6537 CoreWorkResult
6538 CoreWorkCompleted
6539 (constructor
6540 CoreTerm
6541 CoreEliminator
6542 coreEliminatedFamilyName
6543 new_coreEliminatorMotive
6544 new_coreEliminatorScrutinee
6545 new_coreEliminatorBranches)
6546 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.