Source/Packages

Compiler.QuotedLiteral

packages/compiler/src/Compiler/QuotedLiteral.alpha

1,020 lines62 declarations45.0 KiBSHA-256 605e975984e2

def · lines 422–437

decodeByteLiteralBody

Full file
Input includes its closing quote; the full-spelling byte offset starts at2.
422def decodeByteLiteralBody =
423  (lambda unrestricted body : Bytes .
424    (app
425      (bytes-eliminate
426        (lambda unrestricted remaining : Bytes .
427          (pi unrestricted state : (family QuotedByteState) .
428            (pi unrestricted offset : Nat . (family QuotedLiteralResult))))
429        quotedByteFinish
430        (lambda unrestricted head : Byte .
431          (lambda unrestricted tail : Bytes .
432            (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
433              (lambda unrestricted state : (family QuotedByteState) .
434                (lambda unrestricted offset : Nat . (quotedByteStep head state offset continue))))))
435        body)
436      (constructor QuotedByteState QuotedNormal)
437      (succ (succ zero))))

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.