BendMlBpeTokenizer.kn_sub: 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 419-422 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=419&end_line=422

import Base

# if x == a and x is known, a is known too
def kn_sub(+D: List<&2, Rule>, +x: Tk, +a: Tk, ex: {x == a : Tk}, kx: {True{} == kn(D, x) : Bool}) -> {True{} == kn(D, a) : Bool}:
  %ex : {True{} == kn(D, _) : Bool}
  kx

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=kn