def ParsedBytes.prepend

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

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

813# Put the two digits of one more byte in front of the bytes already read: n
814# bytes become 1 + n.
815def ParsedBytes.prepend(-n: Nat, digits: Digits.Digits(2n), parsed: ParsedBytes<n>) -> ParsedBytes<1n+n>:
816  match digits parsed:
817    case Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}} ParsedBytes{rest_digits, rest}:
818      ParsedBytes{Digits.DCon{high, Digits.DCon{low, rest_digits}}, rest}