def Parse.id_bytes.finish

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

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

860# The bytes of a supplied ID must be the whole list, and not all zero.
861def Parse.id_bytes.finish(n: Nat, parsed: ParsedBytes<n>, field: Field) ->
862  Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
863  match parsed:
864    case ParsedBytes{digits, rest}:
865      do Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
866        end : Unit <- Parse.bytes_end(rest)
867        Parse.nonzero(Nat.double(n), digits, field)