Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 1218–1253

combineResolvedApplication

Full file
1218def combineResolvedApplication :
1219  (pi unrestricted functionResult : (family CoreResolutionResult) .
1220    (pi unrestricted argumentResult : (family CoreResolutionResult) . (family CoreResolutionResult))) =
1221  (lambda unrestricted functionResult : (family CoreResolutionResult) .
1222    (lambda unrestricted argumentResult : (family CoreResolutionResult) .
1223      (eliminate
1224        CoreResolutionResult
1225        (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult))
1226        functionResult
1227        (branch
1228          CoreResolved
1229          function
1230          .
1231          (eliminate
1232            CoreResolutionResult
1233            (lambda unrestricted value : (family CoreResolutionResult) .
1234              (family CoreResolutionResult))
1235            argumentResult
1236            (branch
1237              CoreResolved
1238              argument
1239              .
1240              (constructor
1241                CoreResolutionResult
1242                CoreResolved
1243                (constructor CoreTerm CoreApplication function argument)))
1244            (branch
1245              CoreResolutionFailed
1246              identifier
1247              .
1248              (constructor CoreResolutionResult CoreResolutionFailed identifier))))
1249        (branch
1250          CoreResolutionFailed
1251          identifier
1252          .
1253          (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.