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 11193–11205

shiftTypeLookup

Full file
11193def shiftTypeLookup :
11194  (pi unrestricted result : (family TypeLookupResult) . (family TypeLookupResult)) =
11195  (lambda unrestricted result : (family TypeLookupResult) .
11196    (eliminate
11197      TypeLookupResult
11198      (lambda unrestricted value : (family TypeLookupResult) . (family TypeLookupResult))
11199      result
11200      (branch
11201        TypeFound
11202        variableType
11203        .
11204        (constructor TypeLookupResult TypeFound (shiftCoreBy (succ zero) variableType)))
11205      (branch TypeNotFound index . (constructor TypeLookupResult TypeNotFound (succ index)))))

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.