11492def inferUniversePair :
11493 (pi unrestricted domainInspection : (family UniverseInspection) .
11494 (pi unrestricted codomainInspection : (family UniverseInspection) .
11495 (family CoreInferenceResult))) =
11496 (lambda unrestricted domainInspection : (family UniverseInspection) .
11497 (lambda unrestricted codomainInspection : (family UniverseInspection) .
11498 (eliminate
11499 UniverseInspection
11500 (lambda unrestricted inspection : (family UniverseInspection) .
11501 (family CoreInferenceResult))
11502 domainInspection
11503 (branch
11504 IsUniverse
11505 domainLevel
11506 .
11507 (eliminate
11508 UniverseInspection
11509 (lambda unrestricted inspection : (family UniverseInspection) .
11510 (family CoreInferenceResult))
11511 codomainInspection
11512 (branch
11513 IsUniverse
11514 codomainLevel
11515 .
11516 (constructor
11517 CoreInferenceResult
11518 CoreInferred
11519 (constructor CoreTerm CoreUniverse (naturalMaximum domainLevel codomainLevel))))
11520 (branch
11521 NotUniverse
11522 .
11523 (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ zero)))))))
11524 (branch
11525 NotUniverse
11526 .
11527 (constructor CoreInferenceResult CoreInferenceFailed (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.