AlphaGitHub
Source/Packages

Compiler.AST

packages/compiler/src/Compiler/AST.alpha

166 lines117 declarations5.7 KiBSHA-256 a0f24e9809ba
Download exact fileView at revisionf5034773ad4bb52133

def · lines 127–141

parseHead

Full file
127def parseHead =
128  (lambda unrestricted input : Bytes .
129    (bytes-eliminate
130      (lambda unrestricted remaining : Bytes . (family Term))
131      (constructor Term Variable b"")
132      (lambda unrestricted head : Byte .
133        (lambda unrestricted tail : Bytes .
134          (lambda unrestricted parsedTail : (family Term) .
135            (nat-eliminate
136              (lambda unrestricted matched : Nat . (family Term))
137              (constructor Term Variable (bytes-cons head tail))
138              (lambda unrestricted predecessor : Nat .
139                (lambda unrestricted induction : (family Term) . (constructor Term NaturalZero)))
140              (byte-equal head (byte 48))))))
141      input))

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.