def ext_m

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:343

import Base

343# Adding the (new) rule i on top of the table does not change the expansion of a
344# token M{j} that the old table already knows (j != i, because i is new).
345def ext_m(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +j: Nat, h: Bool, eh: {h == Nat.is_eq(i, j) : Bool}, nf: {True{} == Bool.not(has(D, i)) : Bool}, kt: {True{} == has(D, j) : Bool}) -> {exp(Rule{i, a, b} <> D, M{j}) == exp(D, M{j}) : List<&2, Nat>}:
346  match h:
347    case True{}:
348      # h = True means i == j; but j is known (has D j) and i is not (not has D i)
349      +ij = nat_eq_sound(i, j, eh)
350      +hij = Equal.cong(Nat, Bool, k => has(D, k), i, j, ij)
351      +f1 = Equal.trans(Bool, False{}, has(D, i), has(D, j), not_true(has(D, i), nf), hij)
352      +tf = Equal.trans(Bool, True{}, has(D, j), False{}, kt, Equal.sym(Bool, False{}, has(D, j), f1))
353      %tf : BD(_, Unit, {exp.go(Rule{i, a, b} <> D, Cmp.is_eq(Nat.cmp(i, j)), M{j}) == exp.go(D, hits(D, M{j}), M{j}) : List<&2, Nat>})
354      Unit{}
355    case False{}:
356      %eh : {exp.go(Rule{i, a, b} <> D, _, M{j}) == exp(D, M{j}) : List<&2, Nat>}
357      {==}