TraceContext.Parse.bytes: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 833-849 of bend-trace-context@0.2.0.0/trace_context.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&start_line=833&end_line=849

import Base
import bend-trace-context@0.2.0.0/src/digits.bend as Digits

# Consume exactly n cells as bytes, keeping the cells after them. As in
# Parse.digits, the recursion decreases n, so the result's type has the 2n
# digits of n bytes.
def Parse.bytes(n: Nat, bytes: List<&2, U32>, offset: Nat) -> Result<&2, &2, Error, ParsedBytes<n>>:
  match n:
    case 0n:
      Done{ParsedBytes{Digits.DNil{}, bytes}}
    case 1n+p:
      match bytes:
        case Nil{}:
          Fail{UnexpectedEnd{offset}}
        case Con{cell, tail}:
          +at = offset
          do Result<&2, &2, Error, ParsedBytes<1n+p>>:
            digits : Digits.Digits(2n) <- Parse.byte(cell, at)
            parsed : ParsedBytes<p> <- Parse.bytes(p, tail, 1n+at)
            return ParsedBytes.prepend(p, digits, parsed)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.pure
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.byte
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=ParsedBytes
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=ParsedBytes.prepend