Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 1119–1157

combineResolvedLambda

Full file
1119def combineResolvedLambda :
1120  (pi unrestricted multiplicity : (family CoreMultiplicity) .
1121    (pi unrestricted domainResult : (family CoreResolutionResult) .
1122      (pi unrestricted bodyResult : (family CoreResolutionResult) . (family CoreResolutionResult)))) =
1123  (lambda unrestricted multiplicity : (family CoreMultiplicity) .
1124    (lambda unrestricted domainResult : (family CoreResolutionResult) .
1125      (lambda unrestricted bodyResult : (family CoreResolutionResult) .
1126        (eliminate
1127          CoreResolutionResult
1128          (lambda unrestricted value : (family CoreResolutionResult) .
1129            (family CoreResolutionResult))
1130          domainResult
1131          (branch
1132            CoreResolved
1133            domain
1134            .
1135            (eliminate
1136              CoreResolutionResult
1137              (lambda unrestricted value : (family CoreResolutionResult) .
1138                (family CoreResolutionResult))
1139              bodyResult
1140              (branch
1141                CoreResolved
1142                body
1143                .
1144                (constructor
1145                  CoreResolutionResult
1146                  CoreResolved
1147                  (constructor CoreTerm CoreLambda multiplicity domain body)))
1148              (branch
1149                CoreResolutionFailed
1150                identifier
1151                .
1152                (constructor CoreResolutionResult CoreResolutionFailed identifier))))
1153          (branch
1154            CoreResolutionFailed
1155            identifier
1156            .
1157            (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.