def below_fresh

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

import Base

624# not (has D i) when all the ids in D are smaller than i
625def below_fresh(+D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == Bool.not(has(D, i)) : Bool}:
626  %below_has(D, i, e) : {True{} == Bool.not(_) : Bool}
627  {==}