11688def inferApplicationPi :
11689 (pi unrestricted argument : (family CoreTerm) .
11690 (pi unrestricted inspection : (family PiInspection) .
11691 (pi unrestricted argumentResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) =
11692 (lambda unrestricted argument : (family CoreTerm) .
11693 (lambda unrestricted inspection : (family PiInspection) .
11694 (lambda unrestricted argumentResult : (family CoreInferenceResult) .
11695 (eliminate
11696 PiInspection
11697 (lambda unrestricted value : (family PiInspection) . (family CoreInferenceResult))
11698 inspection
11699 (branch
11700 IsPi
11701 multiplicity
11702 domain
11703 codomain
11704 .
11705 (inferApplicationArgument argument domain codomain argumentResult))
11706 (branch
11707 NotPi
11708 .
11709 (constructor
11710 CoreInferenceResult
11711 CoreInferenceFailed
11712 (succ (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.