~/jendhub

def below_has

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

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

605def below_has(D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {False{} == has(D, i) : Bool}:
606  match D:
607    case Nil{}:
608      {==}
609    case Con{Rule{+j, a, b}, +t}:
610      %lt_ne(j, i, and_true_l(Nat.is_lt(j, i), below(t, i), e)) : {False{} == Bool.or(_, has(t, i)) : Bool}
611      below_has(t, i, and_true_r(Nat.is_lt(j, i), below(t, i), e))

Uses (11)

Used by (1)