def lift_dec

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

import Base

494# with no rules, the bytes decode to themselves
495def lift_dec(bs: List<&2, Nat>) -> {dec(Nil{}, lift(bs)) == bs : List<&2, Nat>}:
496  match bs:
497    case Nil{}:
498      {==}
499    case Con{+n, +t}:
500      %lift_dec(t) : {n <> dec(Nil{}, lift(t)) == n <> _ : List<&2, Nat>}
501      {==}