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 1255–1275

combineResolvedNaturalSuccessor

Full file
1255def combineResolvedNaturalSuccessor :
1256  (pi unrestricted predecessorResult : (family CoreResolutionResult) .
1257    (family CoreResolutionResult)) =
1258  (lambda unrestricted predecessorResult : (family CoreResolutionResult) .
1259    (eliminate
1260      CoreResolutionResult
1261      (lambda unrestricted result : (family CoreResolutionResult) . (family CoreResolutionResult))
1262      predecessorResult
1263      (branch
1264        CoreResolved
1265        predecessor
1266        .
1267        (constructor
1268          CoreResolutionResult
1269          CoreResolved
1270          (constructor CoreTerm CoreNaturalSuccessor predecessor)))
1271      (branch
1272        CoreResolutionFailed
1273        identifier
1274        .
1275        (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.