def Parse.id.finish

bend-trace-context@0.2.0.0 · trace_context.bend:516

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

516# The digits of a supplied ID must be the whole text, and not all zero.
517def Parse.id.finish(n: Nat, parsed: Parsed<n>, field: Field) ->
518  Result<&2, &2, Error, Digits.NonZero<n>>:
519  match parsed:
520    case Parsed{digits, rest}:
521      do Result<&2, &2, Error, Digits.NonZero<n>>:
522        end : Unit <- Parse.end(rest)
523        Parse.nonzero(n, digits, field)