11590def inferLambdaFromUniverse :
11591 (pi unrestricted multiplicity : (family CoreMultiplicity) .
11592 (pi unrestricted domain : (family CoreTerm) .
11593 (pi unrestricted inspection : (family UniverseInspection) .
11594 (pi unrestricted bodyResult : (family CoreInferenceResult) . (family CoreInferenceResult))))) =
11595 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
11596 (lambda unrestricted domain : (family CoreTerm) .
11597 (lambda unrestricted inspection : (family UniverseInspection) .
11598 (lambda unrestricted bodyResult : (family CoreInferenceResult) .
11599 (eliminate
11600 UniverseInspection
11601 (lambda unrestricted value : (family UniverseInspection) . (family CoreInferenceResult))
11602 inspection
11603 (branch IsUniverse level . (inferLambdaBody multiplicity domain bodyResult))
11604 (branch
11605 NotUniverse
11606 .
11607 (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ zero)))))))))))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.