4418def reduceCoreWithBudget =
4419 (lambda unrestricted step : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) .
4420 (lambda unrestricted budget : Nat .
4421 (nat-eliminate
4422 (lambda unrestricted remaining : Nat .
4423 (pi unrestricted term : (family CoreTerm) . (family CoreReductionResult)))
4424 (lambda unrestricted term : (family CoreTerm) .
4425 (constructor CoreReductionResult CoreReductionExhausted term zero))
4426 (lambda unrestricted predecessor : Nat .
4427 (lambda unrestricted induction : (pi unrestricted term : (family CoreTerm) . (family CoreReductionResult)) .
4428 (lambda unrestricted term : (family CoreTerm) .
4429 (app
4430 (lambda unrestricted reduced : (family CoreTerm) .
4431 (app
4432 (nat-eliminate
4433 (lambda unrestricted equal : Nat .
4434 (pi unrestricted trigger : Nat . (family CoreReductionResult)))
4435 (lambda unrestricted trigger : Nat .
4436 (countCoreReductionRound (induction reduced)))
4437 (lambda unrestricted prior : Nat .
4438 (lambda unrestricted ignored : (pi unrestricted trigger : Nat . (family CoreReductionResult)) .
4439 (lambda unrestricted trigger : Nat .
4440 (constructor
4441 CoreReductionResult
4442 CoreReductionCompleted
4443 reduced
4444 (succ zero)))))
4445 (coreTermEqual term reduced))
4446 zero))
4447 (step term)))))
4448 budget)))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.