The budget bounds each requested normal form, not aggregate inference work.
11656def inferApplicationArgumentWithBudget =
11657 (lambda unrestricted budget : Nat .
11658 (lambda unrestricted argument : (family CoreTerm) .
11659 (lambda unrestricted domain : (family CoreTerm) .
11660 (lambda unrestricted codomain : (family CoreTerm) .
11661 (lambda unrestricted argumentResult : (family CoreInferenceResult) .
11662 (eliminate
11663 CoreInferenceResult
11664 (lambda unrestricted result : (family CoreInferenceResult) .
11665 (family CoreInferenceResult))
11666 argumentResult
11667 (branch
11668 CoreInferred
11669 argumentType
11670 .
11671 (withCoreNormalization
11672 budget
11673 argumentType
11674 (lambda unrestricted normalArgumentType : (family CoreTerm) .
11675 (withCoreNormalization
11676 budget
11677 domain
11678 (inferApplicationNormalizedDomain budget argument codomain normalArgumentType)))))
11679 (branch
11680 CoreInferenceFailed
11681 code
11682 .
11683 (constructor CoreInferenceResult CoreInferenceFailed code))))))))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.