def fields.after.pick

bend-toon-codec@0.1.0.0 · src/hdr.bend:80

import Base
import bend-toon-codec@0.1.0.0/src/head.bend as Hd
import bend-toon-codec@0.1.0.0/src/split.bend as S

80def fields.after.pick(+colon: Bool, +n: U32, +d: U32, +inner: String, +s: String) -> Result<&2, &2, String, Hdr>:
81  match colon:
82    case True{}:
83      fields.done(n, d, Hd.drop(s), names(d, S.split(inner, d)))
84    case False{}:
85      bad("expected : after the field list")