~/jendhub

def len.ok

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

import bend-toon-codec@0.1.0.0/src/hdr.bend as Hdr
import Base
import bend-toon-codec@0.1.0.0/src/head.bend as Hd

147# A length is `0` or digits without a leading zero, at most nine of them.
148def len.ok(+ds: String) -> Bool:
149  len.ok.pick(String.is_empty(ds), String.eq(ds, "0"), Hd.lead(ds, 48), ds)

Uses (6)

Used by (1)