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 11469–11490

inferNaturalSuccessorType

Full file
11469def inferNaturalSuccessorType :
11470  (pi unrestricted predecessorResult : (family CoreInferenceResult) . (family CoreInferenceResult)) =
11471  (lambda unrestricted predecessorResult : (family CoreInferenceResult) .
11472    (eliminate
11473      CoreInferenceResult
11474      (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult))
11475      predecessorResult
11476      (branch
11477        CoreInferred
11478        predecessorType
11479        .
11480        (nat-eliminate
11481          (lambda unrestricted matched : Nat . (family CoreInferenceResult))
11482          (constructor
11483            CoreInferenceResult
11484            CoreInferenceFailed
11485            (succ (succ (succ (succ (succ (succ (succ zero))))))))
11486          (lambda unrestricted predecessor : Nat .
11487            (lambda unrestricted induction : (family CoreInferenceResult) .
11488              (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreNatural))))
11489          (coreTermEqual predecessorType (constructor CoreTerm CoreNatural))))
11490      (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))

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.