TraceContext.Parse.digits: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 353-370 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=353&end_line=370

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

# Consume exactly n characters as digits, keeping the unconsumed rest of the
# text. The recursion decreases n, so no length check or unchecked conversion
# is needed: the result's type already has length n.
def Parse.digits(n: Nat, text: String, offset: Nat) ->
  Result<&2, &2, Error, Parsed<n>>:
  match n:
    case 0n:
      Done{Parsed{Digits.DNil{}, text}}
    case 1n+p:
      match text:
        case SNil{}:
          Fail{UnexpectedEnd{offset}}
        case SCon{char, tail}:
          +at = offset
          do Result<&2, &2, Error, Parsed<1n+p>>:
            digit : Hex.Digit <- Parse.digit(char, at)
            parsed : Parsed<p> <- Parse.digits(p, tail, 1n+at)
            return Parsed.prepend(p, digit, parsed)

Uses (11):
  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=String
  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/src/hex.bend&name=Digit
  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.digit
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parsed
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parsed.prepend