law dec_append

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:536

import Base

536# LAW 3 (concatenation): decoding two token lists together is decoding
537# each one and joining the bytes.
538law dec_append:
539  for +D: List<&2, Rule>
540  for xs: List<&2, Tk>
541  for +ys: List<&2, Tk>
542  {dec(D, List.append(&2, Tk, xs, ys)) == List.append(&2, Nat, dec(D, xs), dec(D, ys)) : List<&2, Nat>}