def lift_known

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

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

import Base

503def lift_known(bs: List<&2, Nat>) -> {True{} == knl(Nil{}, lift(bs)) : Bool}:
504  match bs:
505    case Nil{}:
506      {==}
507    case Con{n, t}:
508      lift_known(t)

Uses (5)

Used by (2)