BendMlBpeTokenizer.exp_new: 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 398-408 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=398&end_line=408

import Base

# The new token M{i} expands to the expansion of a followed by that of b
# (looking only at the old table D).
def exp_new(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, h: Bool, eh: {h == Nat.is_eq(i, i) : Bool}) -> {exp(Rule{i, a, b} <> D, M{i}) == List.append(&2, Nat, exp(D, a), exp(D, b)) : List<&2, Nat>}:
  match h:
    case True{}:
      %eh : {exp.go(Rule{i, a, b} <> D, _, M{i}) == List.append(&2, Nat, exp(D, a), exp(D, b)) : List<&2, Nat>}
      {==}
    case False{}:
      +f = Equal.trans(Bool, True{}, Nat.is_eq(i, i), False{}, nat_eq_refl(i), Equal.sym(Bool, False{}, Nat.is_eq(i, i), eh))
      %f : BD(_, Unit, {exp(Rule{i, a, b} <> D, M{i}) == List.append(&2, Nat, exp(D, a), exp(D, b)) : List<&2, Nat>})
      Unit{}

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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=BD
  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=exp
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=exp.go
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=nat_eq_refl