AlphaGitHub
Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d
Download exact fileView at revisionf5034773ad4bb52133

def · lines 5855–5878

syntaxOriginDropPrefix

Full file
Removing a synthetic prefix changes coordinates, never token spelling.
5855def syntaxOriginDropPrefix =
5856  (lambda unrestricted prefix : Nat .
5857    (lambda unrestricted origin : (family SyntaxOrigin) .
5858      (eliminate
5859        SyntaxOrigin
5860        (lambda unrestricted current : (family SyntaxOrigin) . (family SyntaxOrigin))
5861        origin
5862        (branch SyntaxOriginUnknown . (constructor SyntaxOrigin SyntaxOriginUnknown))
5863        (branch
5864          SyntaxOriginRange
5865          start
5866          end
5867          .
5868          (nat-eliminate
5869            (lambda unrestricted overlaps : Nat . (family SyntaxOrigin))
5870            (constructor
5871              SyntaxOrigin
5872              SyntaxOriginRange
5873              (Std.Natural/naturalSaturatingSubtract start prefix)
5874              (Std.Natural/naturalSaturatingSubtract end prefix))
5875            (lambda unrestricted predecessor : Nat .
5876              (lambda unrestricted unused : (family SyntaxOrigin) .
5877                (constructor SyntaxOrigin SyntaxOriginUnknown)))
5878            (nat-less-than start prefix))))))

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.