AlphaGitHub
Source/Packages

Compiler.ApplicationBuilder

packages/compiler/src/Compiler/ApplicationBuilder.alpha

767 lines104 declarations33.8 KiBSHA-256 4afcba25576e
Download exact fileView at revisionf5034773ad4bb52133

def · lines 611–628

applicationBuilderScopeContains

Full file
611def applicationBuilderScopeContains :
612  (pi unrestricted scope : (family NameScope) .
613    (pi unrestricted candidate : Bytes . Nat)) =
614  (lambda unrestricted scope : (family NameScope) .
615    (eliminate NameScope
616      (lambda unrestricted value : (family NameScope) .
617        (pi unrestricted candidate : Bytes . Nat))
618      scope
619      (branch EmptyNameScope .
620        (lambda unrestricted candidate : Bytes . zero))
621      (branch NameScopeBinding identifier outer induction .
622        (lambda unrestricted candidate : Bytes .
623          (nat-eliminate
624            (lambda unrestricted matched : Nat . Nat)
625            (app induction candidate)
626            (lambda unrestricted predecessor : Nat .
627              (lambda unrestricted ignored : Nat . (succ zero)))
628            (bytes-equal identifier candidate))))))

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.