1078def combineResolvedPi :
1079 (pi unrestricted multiplicity : (family CoreMultiplicity) .
1080 (pi unrestricted domainResult : (family CoreResolutionResult) .
1081 (pi unrestricted codomainResult : (family CoreResolutionResult) .
1082 (family CoreResolutionResult)))) =
1083 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
1084 (lambda unrestricted domainResult : (family CoreResolutionResult) .
1085 (lambda unrestricted codomainResult : (family CoreResolutionResult) .
1086 (eliminate
1087 CoreResolutionResult
1088 (lambda unrestricted value : (family CoreResolutionResult) .
1089 (family CoreResolutionResult))
1090 domainResult
1091 (branch
1092 CoreResolved
1093 domain
1094 .
1095 (eliminate
1096 CoreResolutionResult
1097 (lambda unrestricted value : (family CoreResolutionResult) .
1098 (family CoreResolutionResult))
1099 codomainResult
1100 (branch
1101 CoreResolved
1102 codomain
1103 .
1104 (constructor
1105 CoreResolutionResult
1106 CoreResolved
1107 (constructor CoreTerm CorePi multiplicity domain codomain)))
1108 (branch
1109 CoreResolutionFailed
1110 identifier
1111 .
1112 (constructor CoreResolutionResult CoreResolutionFailed identifier))))
1113 (branch
1114 CoreResolutionFailed
1115 identifier
1116 .
1117 (constructor CoreResolutionResult CoreResolutionFailed identifier))))))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.