def below_cons

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

import bend-ml-bpe-tokenizer@0.1.3.0/main.bend as BendMlBpeTokenizer

import Base

620# adding the rule with id `next` (greater than all those in `done`) keeps the table "below 1+next"
621def 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}:
622  and_intro(Nat.is_lt(i, 1n+i), below(D, 1n+i), lt_succ(i), below_up(D, i, e))

Uses (10)

Used by (1)

bend-ml-bpe-tokenizer@0.1.3.0/main:tw