~/jendhub

def below_up

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

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

613def below_up(D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == below(D, 1n+i) : Bool}:
614  match D:
615    case Nil{}:
616      {==}
617    case Con{Rule{+j, a, b}, +t}:
618      and_intro(Nat.is_lt(j, 1n+i), below(t, 1n+i), lt_up(j, i, and_true_l(Nat.is_lt(j, i), below(t, i), e)), below_up(t, i, and_true_r(Nat.is_lt(j, i), below(t, i), e)))

Uses (10)

Used by (1)