11529def inferPiType :
11530 (pi unrestricted multiplicity : (family CoreMultiplicity) .
11531 (pi unrestricted domainResult : (family CoreInferenceResult) .
11532 (pi unrestricted codomainResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) =
11533 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
11534 (lambda unrestricted domainResult : (family CoreInferenceResult) .
11535 (lambda unrestricted codomainResult : (family CoreInferenceResult) .
11536 (eliminate
11537 CoreInferenceResult
11538 (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult))
11539 domainResult
11540 (branch
11541 CoreInferred
11542 domainType
11543 .
11544 (eliminate
11545 CoreInferenceResult
11546 (lambda unrestricted result : (family CoreInferenceResult) .
11547 (family CoreInferenceResult))
11548 codomainResult
11549 (branch
11550 CoreInferred
11551 codomainType
11552 .
11553 (inferUniversePair (inspectUniverse domainType) (inspectUniverse codomainType)))
11554 (branch
11555 CoreInferenceFailed
11556 code
11557 .
11558 (constructor CoreInferenceResult CoreInferenceFailed code))))
11559 (branch
11560 CoreInferenceFailed
11561 code
11562 .
11563 (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.