def ext_tok

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

import Base

375# the same for any known token (a byte never depends on the table)
376def ext_tok(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, t: Tk, kt: {True{} == kn(D, t) : Bool}, nf: {True{} == Bool.not(has(D, i)) : Bool}) -> {exp(Rule{i, a, b} <> D, t) == exp(D, t) : List<&2, Nat>}:
377  match D t:
378    case Nil{} B{n}:
379      {==}
380    case Con{Rule{j, a2, b2}, rest} B{n}:
381      {==}
382    case _ M{+j}:
383      ext_m(D, i, a, b, j, Nat.is_eq(i, j), {==}, nf, kt)