BendMlBpeTokenizer.enc_known: def of bend-ml-bpe-tokenizer@0.1.3.0
Import: import bend-ml-bpe-tokenizer@0.1.3.0/main.bend as BendMlBpeTokenizer
Lines 476-482 of bend-ml-bpe-tokenizer@0.1.3.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&start_line=476&end_line=482

import Base

# every emitted token is known to the complete (reversed) table
def enc_known(todo: List<&2, Rule>, +done: List<&2, Rule>, +xs: List<&2, Tk>, +wfe: {True{} == wf.go(todo, done) : Bool}, +kx: {True{} == knl(done, xs) : Bool}) -> {True{} == knl(List.reverse.go(&2, Rule, todo, done), encode.go(todo, done, xs)) : Bool}:
  match todo:
    case Nil{}:
      kx
    case Con{Rule{+i, +a, +b}, +rest}:
      enc_known(rest, Rule{i, a, b} <> done, merge.go(xs, peek(a, b, xs), a, b, M{i}), and_true_r(Bool.not(has(done, i)), wf.go(rest, Rule{i, a, b} <> done), wfe), kp(done, i, a, b, xs, peek(a, b, xs), {==}, kx))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse.go
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Rule
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Tk
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=and_true_r
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=encode.go
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=has
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=knl
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kp
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=merge.go
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=peek
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=wf.go