law train_wf

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

import Base

639# LAW (train_wf): the table that train returns is always well formed, so the roundtrip holds for it
640law train_wf:
641  for n: Nat
642  for +next: Nat
643  for +xs: List<&2, Tk>
644  {True{} == wf(train(n, next, xs)) : Bool}