BendMlBpeTokenizer.below_cons: 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 620-622 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=620&end_line=622

import Base

# adding the rule with id `next` (greater than all those in `done`) keeps the table "below 1+next"
def below_cons(+a: Tk, +b: Tk, +D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == below(Rule{i, a, b} <> D, 1n+i) : Bool}:
  and_intro(Nat.is_lt(i, 1n+i), below(D, 1n+i), lt_succ(i), below_up(D, i, e))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Rule
  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=and_intro
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below_up
  https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lt_succ