Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 1277–1312

combineResolvedTermSequence

Full file
1277def combineResolvedTermSequence :
1278  (pi unrestricted headResult : (family CoreResolutionResult) .
1279    (pi unrestricted tailResult : (family CoreResolutionResult) . (family CoreResolutionResult))) =
1280  (lambda unrestricted headResult : (family CoreResolutionResult) .
1281    (lambda unrestricted tailResult : (family CoreResolutionResult) .
1282      (eliminate
1283        CoreResolutionResult
1284        (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult))
1285        headResult
1286        (branch
1287          CoreResolved
1288          head
1289          .
1290          (eliminate
1291            CoreResolutionResult
1292            (lambda unrestricted value : (family CoreResolutionResult) .
1293              (family CoreResolutionResult))
1294            tailResult
1295            (branch
1296              CoreResolved
1297              tail
1298              .
1299              (constructor
1300                CoreResolutionResult
1301                CoreResolved
1302                (constructor CoreTerm CoreTermSequenceNext head tail)))
1303            (branch
1304              CoreResolutionFailed
1305              identifier
1306              .
1307              (constructor CoreResolutionResult CoreResolutionFailed identifier))))
1308        (branch
1309          CoreResolutionFailed
1310          identifier
1311          .
1312          (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.