11609def inferLambdaType :
11610 (pi unrestricted multiplicity : (family CoreMultiplicity) .
11611 (pi unrestricted domain : (family CoreTerm) .
11612 (pi unrestricted domainResult : (family CoreInferenceResult) .
11613 (pi unrestricted bodyResult : (family CoreInferenceResult) . (family CoreInferenceResult))))) =
11614 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
11615 (lambda unrestricted domain : (family CoreTerm) .
11616 (lambda unrestricted domainResult : (family CoreInferenceResult) .
11617 (lambda unrestricted bodyResult : (family CoreInferenceResult) .
11618 (eliminate
11619 CoreInferenceResult
11620 (lambda unrestricted result : (family CoreInferenceResult) .
11621 (family CoreInferenceResult))
11622 domainResult
11623 (branch
11624 CoreInferred
11625 domainType
11626 .
11627 (inferLambdaFromUniverse multiplicity domain (inspectUniverse domainType) bodyResult))
11628 (branch
11629 CoreInferenceFailed
11630 code
11631 .
11632 (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.