BendMlBpeTokenizer.tk_eq_sound: 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 328-341 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=328&end_line=341

import Base

def tk_eq_sound(+x: Tk, +y: Tk, e: {True{} == Tk.eq(x, y) : Bool}) -> {x == y : Tk}:
  match x y:
    case B{+m} B{+n}:
      %nat_eq_sound(m, n, e) : {B{m} == B{_} : Tk}
      {==}
    case M{+i} M{+j}:
      %nat_eq_sound(i, j, e) : {M{i} == M{_} : Tk}
      {==}
    case B{m} M{j}:
      %e : BD(_, Unit, {B{m} == M{j} : Tk})
      Unit{}
    case M{i} B{n}:
      %e : BD(_, Unit, {M{i} == B{n} : Tk})
      Unit{}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Tk
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Tk.eq
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=nat_eq_sound