def tk_eq_sound
bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:328
import bend-ml-bpe-tokenizer@0.1.3.0/main.bend as BendMlBpeTokenizer
import Base
328def tk_eq_sound(+x: Tk, +y: Tk, e: {True{} == Tk.eq(x, y) : Bool}) -> {x == y : Tk}:
329 match x y:
330 case B{+m} B{+n}:
331 %nat_eq_sound(m, n, e) : {B{m} == B{_} : Tk}
332 {==}
333 case M{+i} M{+j}:
334 %nat_eq_sound(i, j, e) : {M{i} == M{_} : Tk}
335 {==}
336 case B{m} M{j}:
337 %e : BD(_, Unit, {B{m} == M{j} : Tk})
338 Unit{}
339 case M{i} B{n}:
340 %e : BD(_, Unit, {M{i} == B{n} : Tk})
341 Unit{}