AlphaGitHub
Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1314–1335

combineResolvedFamilyApplication

Full file
1314def combineResolvedFamilyApplication :
1315  (pi unrestricted familyName : Bytes .
1316    (pi unrestricted argumentResult : (family CoreResolutionResult) . (family CoreResolutionResult))) =
1317  (lambda unrestricted familyName : Bytes .
1318    (lambda unrestricted argumentResult : (family CoreResolutionResult) .
1319      (eliminate
1320        CoreResolutionResult
1321        (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult))
1322        argumentResult
1323        (branch
1324          CoreResolved
1325          arguments
1326          .
1327          (constructor
1328            CoreResolutionResult
1329            CoreResolved
1330            (constructor CoreTerm CoreFamilyApplication familyName arguments)))
1331        (branch
1332          CoreResolutionFailed
1333          identifier
1334          .
1335          (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.