Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d

def · lines 4308–4333

decodeNonArithmeticVariableHead

Full file
4308def decodeNonArithmeticVariableHead =
4309  (lambda unrestricted spelling : Bytes .
4310    (lambda unrestricted functionTerm : (family Term) .
4311      (lambda unrestricted argumentTerm : (family Term) .
4312        (lambda unrestricted remaining : (family TermList) .
4313          (chooseNamedDecode
4314            (bytesEqual spelling doSpelling)
4315            (lambda unrestricted force : Nat . (decodeDoApplication argumentTerm remaining))
4316            (lambda unrestricted force : Nat .
4317              (chooseNamedDecode
4318                (bytesEqual spelling letStarSpelling)
4319                (lambda unrestricted force : Nat .
4320                  (decodeLocalLetSequence
4321                    (constructor TermList TermListNext argumentTerm remaining)))
4322                (lambda unrestricted force : Nat .
4323                  (chooseNamedDecode
4324                    (bytesEqual spelling lambdaSpelling)
4325                    (lambda unrestricted force : Nat .
4326                      (decodeBinderForm zero argumentTerm remaining))
4327                    (lambda unrestricted force : Nat .
4328                      (chooseNamedDecode
4329                        (bytesEqual spelling piSpelling)
4330                        (lambda unrestricted force : Nat .
4331                          (decodeBinderForm (succ zero) argumentTerm remaining))
4332                        (lambda unrestricted force : Nat .
4333                          (decodeNonBinderVariableHead spelling functionTerm argumentTerm remaining)))))))))))))

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.